Definition df-had 1380

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

Assertion

Ref	Expression
df-had	|- (hadd(ph, ps, ch) <-> ((ph \/_ ps) \/_ ch))

Detailed syntax breakdown of Definition df-had

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3		wch	. . 3 wff ch
4	1, 2, 3	whad 1378	. 2 wff hadd(ph, ps, ch)
5	1, 2	wxo 1304	. . 3 wff (ph \/_ ps)
6	5, 3	wxo 1304	. 2 wff ((ph \/_ ps) \/_ ch)
7	4, 6	wb 176	1 wff (hadd(ph, ps, ch) <-> ((ph \/_ ps) \/_ ch))

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