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(ph, ps, ch) <-> ((ph /\ ps) \/ (ch /\ (ph \/_ ps))))

Detailed syntax breakdown of Definition df-cad

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3		wch	. . 3 wff ch
4	1, 2, 3	wcad 1379	. 2 wff cadd(ph, ps, ch)
5	1, 2	wa 358	. . 3 wff (ph /\ ps)
6	1, 2	wxo 1304	. . . 4 wff (ph \/_ ps)
7	3, 6	wa 358	. . 3 wff (ch /\ (ph \/_ ps))
8	5, 7	wo 357	. 2 wff ((ph /\ ps) \/ (ch /\ (ph \/_ ps)))
9	4, 8	wb 176	1 wff (cadd(ph, ps, ch) <-> ((ph /\ ps) \/ (ch /\ (ph \/_ ps))))

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