Definition df-cad 1630

Description: Definition of the "carry" output of the full adder. It is true when at least two arguments are true, so it is equal to the "majority" function on three variables. See cador 1631 and cadan 1632 for alternate definitions. (Contributed by Mario Carneiro, 4-Sep-2016.)

Assertion

Ref	Expression
df-cad	⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓))))

Detailed syntax breakdown of Definition df-cad

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3		wch	. . 3 wff 𝜒
4	1, 2, 3	wcad 1629	. 2 wff cadd(𝜑, 𝜓, 𝜒)
5	1, 2	wa 400	. . 3 wff (𝜑 ∧ 𝜓)
6	1, 2	wxo 1534	. . . 4 wff (𝜑 ⊻ 𝜓)
7	3, 6	wa 400	. . 3 wff (𝜒 ∧ (𝜑 ⊻ 𝜓))
8	5, 7	wo 860	. 2 wff ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓)))
9	4, 8	wb 209	1 wff (cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓))))

This definition is referenced by:  cador  1631  cadbi123d  1633  cadcoma  1635  cad11  1639  cad0  1641