Theorem cad0 1400

Description: If one parameter is false, the adder carry is true exactly when both of the other two parameters are true. (Contributed by Mario Carneiro, 8-Sep-2016.)

Assertion

Ref	Expression
cad0	|- (-. ch -> (cadd(ph, ps, ch) <-> (ph /\ ps)))

Proof of Theorem cad0

Step	Hyp	Ref	Expression
1		df-cad 1381	. 2 |- (cadd(ph, ps, ch) <-> ((ph /\ ps) \/ (ch /\ (ph \/_ ps))))
2		idd 21	. . . 4 |- (-. ch -> ((ph /\ ps) -> (ph /\ ps)))
3		pm2.21 100	. . . . 5 |- (-. ch -> (ch -> (ph /\ ps)))
4	3	adantrd 454	. . . 4 |- (-. ch -> ((ch /\ (ph \/_ ps)) -> (ph /\ ps)))
5	2, 4	jaod 369	. . 3 |- (-. ch -> (((ph /\ ps) \/ (ch /\ (ph \/_ ps))) -> (ph /\ ps)))
6		orc 374	. . 3 |- ((ph /\ ps) -> ((ph /\ ps) \/ (ch /\ (ph \/_ ps))))
7	5, 6	impbid1 194	. 2 |- (-. ch -> (((ph /\ ps) \/ (ch /\ (ph \/_ ps))) <-> (ph /\ ps)))
8	1, 7	syl5bb 248	1 |- (-. ch -> (cadd(ph, ps, ch) <-> (ph /\ ps)))

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   \/ wo 357   /\ wa 358   \/_ wxo 1304  caddwcad 1379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-cad 1381

This theorem is referenced by: (None)