Definition df-cad 1608

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 1609 and cadan 1610 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 1607	. 2 wff cadd(𝜑, 𝜓, 𝜒)
5	1, 2	wa 396	. . 3 wff (𝜑 ∧ 𝜓)
6	1, 2	wxo 1509	. . . 4 wff (𝜑 ⊻ 𝜓)
7	3, 6	wa 396	. . 3 wff (𝜒 ∧ (𝜑 ⊻ 𝜓))
8	5, 7	wo 845	. 2 wff ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓)))
9	4, 8	wb 205	1 wff (cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓))))

This definition is referenced by:  cador  1609  cadbi123d  1611  cadcoma  1613  cad11  1617  cad0  1619  cad0OLD  1620