Metamath Proof Explorer

Theorem xor3

Description: Two ways to express "exclusive or". (Contributed by NM, 1-Jan-2006)

Ref Expression
Assertion xor3 ( ¬ ( 𝜑 ↔ 𝜓 ) ↔ ( 𝜑 ↔ ¬ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 pm5.18 ⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( 𝜑 ↔ ¬ 𝜓 ) )
2 1 con2bii ⊢ ( ( 𝜑 ↔ ¬ 𝜓 ) ↔ ¬ ( 𝜑 ↔ 𝜓 ) )
3 2 bicomi ⊢ ( ¬ ( 𝜑 ↔ 𝜓 ) ↔ ( 𝜑 ↔ ¬ 𝜓 ) )