Metamath Proof Explorer

Theorem had0

Description: If the first input is false, then the adder sum is equivalent to the exclusive disjunction of the other two inputs, and conversely. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 12-Jul-2020) Strengthen to a biconditional. (Revised by BJ, 10-Aug-2026)

Ref Expression
Assertion had0 ⊢ ¬ φ ↔ hadd φ ψ χ ↔ ψ ⊻ χ

Proof

Step Hyp Ref Expression
1 hadrot ⊢ hadd φ ψ χ ↔ hadd ψ χ φ
2 df-had ⊢ hadd ψ χ φ ↔ ψ ⊻ χ ⊻ φ
3 df-xor ⊢ ψ ⊻ χ ⊻ φ ↔ ¬ ψ ⊻ χ ↔ φ
4 xor3 ⊢ ¬ ψ ⊻ χ ↔ φ ↔ ψ ⊻ χ ↔ ¬ φ
5 3 4 bitri ⊢ ψ ⊻ χ ⊻ φ ↔ ψ ⊻ χ ↔ ¬ φ
6 2 5 bitri ⊢ hadd ψ χ φ ↔ ψ ⊻ χ ↔ ¬ φ
7 1 6 bitri ⊢ hadd φ ψ χ ↔ ψ ⊻ χ ↔ ¬ φ
8 biass ⊢ hadd φ ψ χ ↔ ψ ⊻ χ ↔ ¬ φ ↔ hadd φ ψ χ ↔ ψ ⊻ χ ↔ ¬ φ
9 7 8 mpbir ⊢ hadd φ ψ χ ↔ ψ ⊻ χ ↔ ¬ φ
10 9 bicomi ⊢ ¬ φ ↔ hadd φ ψ χ ↔ ψ ⊻ χ