This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pm5.16

Description: Theorem *5.16 of WhiteheadRussell p. 124. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 17-Oct-2013)

Ref Expression
Assertion pm5.16 ⊢ ¬ φ ↔ ψ ∧ φ ↔ ¬ ψ

Proof

Step Hyp Ref Expression
1 pm5.18 ⊢ φ ↔ ψ ↔ ¬ φ ↔ ¬ ψ
2 1 biimpi ⊢ φ ↔ ψ → ¬ φ ↔ ¬ ψ
3 imnan ⊢ φ ↔ ψ → ¬ φ ↔ ¬ ψ ↔ ¬ φ ↔ ψ ∧ φ ↔ ¬ ψ
4 2 3 mpbi ⊢ ¬ φ ↔ ψ ∧ φ ↔ ¬ ψ