Metamath Proof Explorer


Theorem xorcomOLD

Description: Obsolete version of xorcom as of 21-Apr-2024. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion xorcomOLD ( ( 𝜑𝜓 ) ↔ ( 𝜓𝜑 ) )

Proof

Step Hyp Ref Expression
1 bicom ( ( 𝜑𝜓 ) ↔ ( 𝜓𝜑 ) )
2 1 notbii ( ¬ ( 𝜑𝜓 ) ↔ ¬ ( 𝜓𝜑 ) )
3 df-xor ( ( 𝜑𝜓 ) ↔ ¬ ( 𝜑𝜓 ) )
4 df-xor ( ( 𝜓𝜑 ) ↔ ¬ ( 𝜓𝜑 ) )
5 2 3 4 3bitr4i ( ( 𝜑𝜓 ) ↔ ( 𝜓𝜑 ) )