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 ⊢ φ ↔ ψ ⊻ χ ↔ φ ⊻ ψ ↔ χ