Definition df-cad 1614

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 1615 and cadan 1616 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 1613	. 2 wff cadd(𝜑, 𝜓, 𝜒)
5	1, 2	wa 399	. . 3 wff (𝜑 ∧ 𝜓)
6	1, 2	wxo 1507	. . . 4 wff (𝜑 ⊻ 𝜓)
7	3, 6	wa 399	. . 3 wff (𝜒 ∧ (𝜑 ⊻ 𝜓))
8	5, 7	wo 847	. 2 wff ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓)))
9	4, 8	wb 209	1 wff (cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓))))

This definition is referenced by:  cador  1615  cadbi123d  1617  cadcoma  1619  cad11  1623  cad0  1625  cad0OLD  1626