theory L. -- Propositional calculus (Logic), Mendelson, p.31:

  formal system.
    atom 𝕗, 𝕥. -- False, true. Not in core of theory L.
  
    formula A, B, C.

  -- These axioms are called A1-A3 in Mendelson:
  axiom L1. A ⇒ (B ⇒ A).
  axiom L2. (A ⇒ (B ⇒ C)) ⇒ ((A ⇒ B) ⇒ (A ⇒ C)).
  axiom L3. (¬ B ⇒ ¬ A) ⇒ ((¬ B ⇒ A) ⇒ B).
    
  -- Modus ponens:
  rule MP. A, A ⇒ B ⊢ B.

  -- `deduction theorem' `1.8'
  -- Entered as an axiom in the absence of the appropriate metatools.
  postulate DT. formula A, B. (A ⊢ B) ⊢ A ⇒ B.

  definition D1. A ∧ B ≔ ¬(A ⇒ ¬ B).  
  definition D2. A ∨ B ≔ (¬ A) ⇒ B.
  definition D3. A ⇔ B ≔ (A ⇒ B) ∧ (B ⇒ A).
  axiom D4. 𝕥.
  definition D5. 𝕗 ≔ ¬ 𝕥.

  rule A1. A, B ⊢ A ∧ B.  -- Test only.

  end formal system.

end theory L.