Definition df-cad 1537

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 1538 and cadan 1539 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 1536	. 2 wff cadd(𝜑, 𝜓, 𝜒)
5	1, 2	wa 383	. . 3 wff (𝜑 ∧ 𝜓)
6	1, 2	wxo 1456	. . . 4 wff (𝜑 ⊻ 𝜓)
7	3, 6	wa 383	. . 3 wff (𝜒 ∧ (𝜑 ⊻ 𝜓))
8	5, 7	wo 382	. 2 wff ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓)))
9	4, 8	wb 195	1 wff (cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓))))

This definition is referenced by:  cador  1538  cadbi123d  1540  cadcoma  1542  cad0  1547  cad11  1549