Definition df-had 1380

Description: Define the half adder (triple XOR). (Contributed by Mario Carneiro, 4-Sep-2016.)

Assertion

Ref	Expression
df-had	⊢ (hadd(φ, ψ, χ) ↔ ((φ ⊻ ψ) ⊻ χ))

Detailed syntax breakdown of Definition df-had

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		wps	. . 3 wff ψ
3		wch	. . 3 wff χ
4	1, 2, 3	whad 1378	. 2 wff hadd(φ, ψ, χ)
5	1, 2	wxo 1304	. . 3 wff (φ ⊻ ψ)
6	5, 3	wxo 1304	. 2 wff ((φ ⊻ ψ) ⊻ χ)
7	4, 6	wb 176	1 wff (hadd(φ, ψ, χ) ↔ ((φ ⊻ ψ) ⊻ χ))

This definition is referenced by:  hadbi123d  1382  hadass  1386  hadbi  1387  hadcoma  1388  hadnot  1393