Definition df-had 1596

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.)

Assertion

Ref	Expression
df-had	⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ⊻ 𝜓) ⊻ 𝜒))

Detailed syntax breakdown of Definition df-had

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3		wch	. . 3 wff 𝜒
4	1, 2, 3	whad 1595	. 2 wff hadd(𝜑, 𝜓, 𝜒)
5	1, 2	wxo 1503	. . 3 wff (𝜑 ⊻ 𝜓)
6	5, 3	wxo 1503	. 2 wff ((𝜑 ⊻ 𝜓) ⊻ 𝜒)
7	4, 6	wb 205	1 wff (hadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ⊻ 𝜓) ⊻ 𝜒))

This definition is referenced by:  hadbi123d  1597  hadass  1599  hadbi  1600  hadcomaOLD  1602