Definition df-cad 1381

Description: Define the half adder carry, which is true when at least two arguments are true. (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 1379	. 2 wff cadd(φ, ψ, χ)
5	1, 2	wa 358	. . 3 wff (φ ∧ ψ)
6	1, 2	wxo 1304	. . . 4 wff (φ ⊻ ψ)
7	3, 6	wa 358	. . 3 wff (χ ∧ (φ ⊻ ψ))
8	5, 7	wo 357	. 2 wff ((φ ∧ ψ) ∨ (χ ∧ (φ ⊻ ψ)))
9	4, 8	wb 176	1 wff (cadd(φ, ψ, χ) ↔ ((φ ∧ ψ) ∨ (χ ∧ (φ ⊻ ψ))))

This definition is referenced by:  cadbi123d  1383  cador  1391  cadcoma  1395  cad1  1398  cad11  1399  cad0  1400