Metamath Proof Explorer

Theorem pm5.18

Description: Theorem *5.18 of WhiteheadRussell p. 124. This theorem says that logical equivalence is the same as negated "exclusive or". (Contributed by NM, 28-Jun-2002) (Proof shortened by Andrew Salmon, 20-Jun-2011) (Proof shortened by Wolf Lammen, 15-Oct-2013)

Ref Expression
Assertion pm5.18 ⊢ φ ↔ ψ ↔ ¬ φ ↔ ¬ ψ

Proof

Step Hyp Ref Expression
1 pm5.501 ⊢ φ → ¬ ψ ↔ φ ↔ ¬ ψ
2 1 con1bid ⊢ φ → ¬ φ ↔ ¬ ψ ↔ ψ
3 pm5.501 ⊢ φ → ψ ↔ φ ↔ ψ
4 2 3 bitr2d ⊢ φ → φ ↔ ψ ↔ ¬ φ ↔ ¬ ψ
5 nbn2 ⊢ ¬ φ → ¬ ¬ ψ ↔ φ ↔ ¬ ψ
6 5 con1bid ⊢ ¬ φ → ¬ φ ↔ ¬ ψ ↔ ¬ ψ
7 nbn2 ⊢ ¬ φ → ¬ ψ ↔ φ ↔ ψ
8 6 7 bitr2d ⊢ ¬ φ → φ ↔ ψ ↔ ¬ φ ↔ ¬ ψ
9 4 8 pm2.61i ⊢ φ ↔ ψ ↔ ¬ φ ↔ ¬ ψ