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 ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ⊻ 𝜓 ) ⊻ 𝜒 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1		wps	⊢ 𝜓
2		wch	⊢ 𝜒
3	0 1 2	whad	⊢ hadd ( 𝜑 , 𝜓 , 𝜒 )
4	0 1	wxo	⊢ ( 𝜑 ⊻ 𝜓 )
5	4 2	wxo	⊢ ( ( 𝜑 ⊻ 𝜓 ) ⊻ 𝜒 )
6	3 5	wb	⊢ ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ⊻ 𝜓 ) ⊻ 𝜒 ) )