Theorem cad1 1398

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

Assertion

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

Proof of Theorem cad1

Step	Hyp	Ref	Expression
1		ibar 490	. . . 4 |- (ch -> ((ph \/_ ps) <-> (ch /\ (ph \/_ ps))))
2	1	bicomd 192	. . 3 |- (ch -> ((ch /\ (ph \/_ ps)) <-> (ph \/_ ps)))
3	2	orbi2d 682	. 2 |- (ch -> (((ph /\ ps) \/ (ch /\ (ph \/_ ps))) <-> ((ph /\ ps) \/ (ph \/_ ps))))
4		df-cad 1381	. 2 |- (cadd(ph, ps, ch) <-> ((ph /\ ps) \/ (ch /\ (ph \/_ ps))))
5		pm5.63 890	. . 3 |- (((ph /\ ps) \/ (ph \/ ps)) <-> ((ph /\ ps) \/ (-. (ph /\ ps) /\ (ph \/ ps))))
6		olc 373	. . . 4 |- ((ph \/ ps) -> ((ph /\ ps) \/ (ph \/ ps)))
7		orc 374	. . . . . 6 |- (ph -> (ph \/ ps))
8	7	adantr 451	. . . . 5 |- ((ph /\ ps) -> (ph \/ ps))
9		id 19	. . . . 5 |- ((ph \/ ps) -> (ph \/ ps))
10	8, 9	jaoi 368	. . . 4 |- (((ph /\ ps) \/ (ph \/ ps)) -> (ph \/ ps))
11	6, 10	impbii 180	. . 3 |- ((ph \/ ps) <-> ((ph /\ ps) \/ (ph \/ ps)))
12		xor2 1310	. . . . 5 |- ((ph \/_ ps) <-> ((ph \/ ps) /\ -. (ph /\ ps)))
13		ancom 437	. . . . 5 |- (((ph \/ ps) /\ -. (ph /\ ps)) <-> (-. (ph /\ ps) /\ (ph \/ ps)))
14	12, 13	bitri 240	. . . 4 |- ((ph \/_ ps) <-> (-. (ph /\ ps) /\ (ph \/ ps)))
15	14	orbi2i 505	. . 3 |- (((ph /\ ps) \/ (ph \/_ ps)) <-> ((ph /\ ps) \/ (-. (ph /\ ps) /\ (ph \/ ps))))
16	5, 11, 15	3bitr4i 268	. 2 |- ((ph \/ ps) <-> ((ph /\ ps) \/ (ph \/_ ps)))
17	3, 4, 16	3bitr4g 279	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-xor 1305  df-cad 1381

This theorem is referenced by: (None)