AAAAAAAAA.calccheck

Proof:
    p ⇒ (q ⇒ r)
  ≡⟨ “Material implication” ⟩ 
    ¬ p ∨ (q ⇒ r)
  ≡⟨ “Material implication” ⟩ 
    ¬ p ∨ (¬ q ∨ r)
  ≡⟨ “Distributivity of ∨ over ∨” ⟩ 
    (¬ p ∨ ¬ q) ∨ (¬ p ∨ r)
  ≡⟨ “Definition of ¬ from ≡” ⟩
    (¬ p ∨ (q ≡ false)) ∨ (¬ p ∨ r)
  ≡⟨ “Distributivity of ∨ over ≡” ⟩ 
    ((¬ p ∨ q) ≡ (¬ p ∨ false)) ∨ (¬ p ∨ r)
  ≡⟨ “Identity of ∨” ⟩
    ((¬ p ∨ q) ≡ ¬ p ) ∨ (¬ p ∨ r)
  ≡⟨ “Distributivity of ∨ over ≡” ⟩
    (¬ p ∨ q)  ∨ (¬ p ∨ r) ≡ ¬ p ∨ ¬ p ∨ r
  ≡⟨ “Idempotency of ∨” ⟩
    (¬ p ∨ q)  ∨ (¬ p ∨ r) ≡ ¬ p ∨ r
  ≡⟨ ? ⟩ 
    ¬ (¬ p ∨ q) ∨ (¬ p ∨ r)
  ≡⟨ ? ⟩
    (p ⇒ q) ⇒ (p ⇒ r)