Definition df-had 1533

Description: Definition of the "sum" output of the full adder (triple exclusive disjunction, or XOR3). (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 1532	. 2 wff hadd ( ph , ps , ch )
5	1, 2	wxo 1464	. . 3 wff ( ph \/_ ps )
6	5, 3	wxo 1464	. 2 wff ( ( ph \/_ ps ) \/_ ch )
7	4, 6	wb 196	1 wff (hadd ( ph , ps , ch ) <-> ( ( ph \/_ ps ) \/_ ch ) )

This definition is referenced by:  hadbi123d  1534  hadass  1536  hadbi  1537  hadcoma  1538