Metamath Proof Explorer


Theorem bj-bixor

Description: Equivalence of two ternary operations. Note the identical order and parenthesizing of the three arguments in both expressions. (Contributed by BJ, 31-Dec-2023)

Ref Expression
Assertion bj-bixor ( ( 𝜑 ↔ ( 𝜓𝜒 ) ) ↔ ( 𝜑 ⊻ ( 𝜓𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 pm5.18 ( ( 𝜑 ↔ ( 𝜓𝜒 ) ) ↔ ¬ ( 𝜑 ↔ ¬ ( 𝜓𝜒 ) ) )
2 1 con2bii ( ( 𝜑 ↔ ¬ ( 𝜓𝜒 ) ) ↔ ¬ ( 𝜑 ↔ ( 𝜓𝜒 ) ) )
3 df-xor ( ( 𝜓𝜒 ) ↔ ¬ ( 𝜓𝜒 ) )
4 3 bibi2i ( ( 𝜑 ↔ ( 𝜓𝜒 ) ) ↔ ( 𝜑 ↔ ¬ ( 𝜓𝜒 ) ) )
5 df-xor ( ( 𝜑 ⊻ ( 𝜓𝜒 ) ) ↔ ¬ ( 𝜑 ↔ ( 𝜓𝜒 ) ) )
6 2 4 5 3bitr4i ( ( 𝜑 ↔ ( 𝜓𝜒 ) ) ↔ ( 𝜑 ⊻ ( 𝜓𝜒 ) ) )