Metamath Proof Explorer


Theorem excxor

Description: This tautology shows that xor is really exclusive. (Contributed by FL, 22-Nov-2010)

Ref Expression
Assertion excxor ( ( 𝜑𝜓 ) ↔ ( ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( ¬ 𝜑𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 df-xor ( ( 𝜑𝜓 ) ↔ ¬ ( 𝜑𝜓 ) )
2 xor ( ¬ ( 𝜑𝜓 ) ↔ ( ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( 𝜓 ∧ ¬ 𝜑 ) ) )
3 ancom ( ( 𝜓 ∧ ¬ 𝜑 ) ↔ ( ¬ 𝜑𝜓 ) )
4 3 orbi2i ( ( ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( 𝜓 ∧ ¬ 𝜑 ) ) ↔ ( ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( ¬ 𝜑𝜓 ) ) )
5 1 2 4 3bitri ( ( 𝜑𝜓 ) ↔ ( ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( ¬ 𝜑𝜓 ) ) )