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 ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑 ↔ ( 𝜓 ↔ 𝜒 ) ) ) |
| 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 ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑 ↔ ( 𝜓 ↔ 𝜒 ) ) ) |