Metamath Proof Explorer


Theorem xorbi12d

Description: Equality property for exclusive disjunction. (Contributed by Mario Carneiro, 4-Sep-2016)

Ref Expression
Hypotheses xor12d.1 ( 𝜑 → ( 𝜓𝜒 ) )
xor12d.2 ( 𝜑 → ( 𝜃𝜏 ) )
Assertion xorbi12d ( 𝜑 → ( ( 𝜓𝜃 ) ↔ ( 𝜒𝜏 ) ) )

Proof

Step Hyp Ref Expression
1 xor12d.1 ( 𝜑 → ( 𝜓𝜒 ) )
2 xor12d.2 ( 𝜑 → ( 𝜃𝜏 ) )
3 1 2 bibi12d ( 𝜑 → ( ( 𝜓𝜃 ) ↔ ( 𝜒𝜏 ) ) )
4 3 notbid ( 𝜑 → ( ¬ ( 𝜓𝜃 ) ↔ ¬ ( 𝜒𝜏 ) ) )
5 df-xor ( ( 𝜓𝜃 ) ↔ ¬ ( 𝜓𝜃 ) )
6 df-xor ( ( 𝜒𝜏 ) ↔ ¬ ( 𝜒𝜏 ) )
7 4 5 6 3bitr4g ( 𝜑 → ( ( 𝜓𝜃 ) ↔ ( 𝜒𝜏 ) ) )