Metamath Proof Explorer

Theorem wl-3xorbi

Description: Triple xor can be replaced with a triple biconditional. Unlike \/_ , you cannot add more inputs by simply stacking up more biconditionals, and still express an "odd number of inputs". (Contributed by Wolf Lammen, 24-Apr-2024)

Ref Expression
Assertion wl-3xorbi ⊢ hadd φ ψ χ ↔ φ ↔ ψ ↔ χ

Proof

Step Hyp Ref Expression
1 wl-df3xor2 ⊢ hadd φ ψ χ ↔ φ ⊻ ψ ⊻ χ
2 df-xor ⊢ φ ⊻ ψ ⊻ χ ↔ ¬ φ ↔ ψ ⊻ χ
3 xor3 ⊢ ¬ φ ↔ ψ ⊻ χ ↔ φ ↔ ¬ ψ ⊻ χ
4 xnor ⊢ ψ ↔ χ ↔ ¬ ψ ⊻ χ
5 4 bibi2i ⊢ φ ↔ ψ ↔ χ ↔ φ ↔ ¬ ψ ⊻ χ
6 3 5 bitr4i ⊢ ¬ φ ↔ ψ ⊻ χ ↔ φ ↔ ψ ↔ χ
7 1 2 6 3bitri ⊢ hadd φ ψ χ ↔ φ ↔ ψ ↔ χ