Metamath Proof Explorer

Theorem wl-df3xor2

Description: Alternative definition of wl-df-3xor , using triple exclusive disjunction, or XOR3. You can add more input by appending each one with a \/_ . Copy of hadass . (Contributed by Mario Carneiro, 4-Sep-2016) df-had redefined. (Revised by Wolf Lammen, 1-May-2024)

Ref Expression
Assertion wl-df3xor2 ⊢ hadd φ ψ χ ↔ φ ⊻ ψ ⊻ χ

Proof

Step Hyp Ref Expression
1 ifpn ⊢ if- φ ¬ ψ ⊻ χ ψ ⊻ χ ↔ if- ¬ φ ψ ⊻ χ ¬ ψ ⊻ χ
2 wl-df-3xor ⊢ hadd φ ψ χ ↔ if- φ ¬ ψ ⊻ χ ψ ⊻ χ
3 df-xor ⊢ φ ⊻ ψ ⊻ χ ↔ ¬ φ ↔ ψ ⊻ χ
4 nbbn ⊢ ¬ φ ↔ ψ ⊻ χ ↔ ¬ φ ↔ ψ ⊻ χ
5 ifpdfbi ⊢ ¬ φ ↔ ψ ⊻ χ ↔ if- ¬ φ ψ ⊻ χ ¬ ψ ⊻ χ
6 3 4 5 3bitr2i ⊢ φ ⊻ ψ ⊻ χ ↔ if- ¬ φ ψ ⊻ χ ¬ ψ ⊻ χ
7 1 2 6 3bitr4i ⊢ hadd φ ψ χ ↔ φ ⊻ ψ ⊻ χ