Definition df-had

Description: Definition of the "sum" output of the full adder (triple exclusive disjunction, or XOR3, or testing whether an odd number of parameters are true). (Contributed by Mario Carneiro, 4-Sep-2016)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	|- ph
1		wps	|- ps
2		wch	|- ch
3	0 1 2	whad	|- hadd ( ph , ps , ch )
4	0 1	wxo	|- ( ph \/_ ps )
5	4 2	wxo	|- ( ( ph \/_ ps ) \/_ ch )
6	3 5	wb	|- ( hadd ( ph , ps , ch ) <-> ( ( ph \/_ ps ) \/_ ch ) )