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\left(\phi ,\psi ,\chi \right)\leftrightarrow \left(\left(\phi ⊻\psi \right)⊻\chi \right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	$$wff\phi$$
1		wps	$$wff\psi$$
2		wch	$$wff\chi$$
3	0 1 2	whad	$$wffhadd\left(\phi ,\psi ,\chi \right)$$
4	0 1	wxo	$$wff\left(\phi ⊻\psi \right)$$
5	4 2	wxo	$$wff\left(\left(\phi ⊻\psi \right)⊻\chi \right)$$
6	3 5	wb	$$wff\left(hadd\left(\phi ,\psi ,\chi \right)\leftrightarrow \left(\left(\phi ⊻\psi \right)⊻\chi \right)\right)$$