Metamath Proof Explorer


Theorem xorbi12iOLD

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

Ref Expression
Hypotheses xorbi12.1 ( 𝜑𝜓 )
xorbi12.2 ( 𝜒𝜃 )
Assertion xorbi12iOLD ( ( 𝜑𝜒 ) ↔ ( 𝜓𝜃 ) )

Proof

Step Hyp Ref Expression
1 xorbi12.1 ( 𝜑𝜓 )
2 xorbi12.2 ( 𝜒𝜃 )
3 1 2 bibi12i ( ( 𝜑𝜒 ) ↔ ( 𝜓𝜃 ) )
4 3 notbii ( ¬ ( 𝜑𝜒 ) ↔ ¬ ( 𝜓𝜃 ) )
5 df-xor ( ( 𝜑𝜒 ) ↔ ¬ ( 𝜑𝜒 ) )
6 df-xor ( ( 𝜓𝜃 ) ↔ ¬ ( 𝜓𝜃 ) )
7 4 5 6 3bitr4i ( ( 𝜑𝜒 ) ↔ ( 𝜓𝜃 ) )