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