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 φ ψ χ φ ψ χ