Definition df-cad 1639

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 1640 and cadan 1641 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 1638	. 2 wff cadd(𝜑, 𝜓, 𝜒)
5	1, 2	wa 401	. . 3 wff (𝜑 ∧ 𝜓)
6	1, 2	wxo 1540	. . . 4 wff (𝜑 ⊻ 𝜓)
7	3, 6	wa 401	. . 3 wff (𝜒 ∧ (𝜑 ⊻ 𝜓))
8	5, 7	wo 861	. 2 wff ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓)))
9	4, 8	wb 209	1 wff (cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓))))

This definition is used by:  cador  1640  cadbi123d  1642  cadcoma  1644  cad11  1648  cad0  1650