Theorem cadan 1392

Description: Write the adder carry in conjunctive normal form. (Contributed by Mario Carneiro, 4-Sep-2016.)

Assertion

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

Proof of Theorem cadan

Step	Hyp	Ref	Expression
1		ordi 834	. . . 4 |- ((((ph /\ ps) \/ (ph /\ ch)) \/ (ps /\ ch)) <-> ((((ph /\ ps) \/ (ph /\ ch)) \/ ps) /\ (((ph /\ ps) \/ (ph /\ ch)) \/ ch)))
2		ordir 835	. . . . . 6 |- (((ph /\ ch) \/ ps) <-> ((ph \/ ps) /\ (ch \/ ps)))
3		simpr 447	. . . . . . . . . . 11 |- ((ph /\ ps) -> ps)
4	3	con3i 127	. . . . . . . . . 10 |- (-. ps -> -. (ph /\ ps))
5		biorf 394	. . . . . . . . . 10 |- (-. (ph /\ ps) -> ((ph /\ ch) <-> ((ph /\ ps) \/ (ph /\ ch))))
6	4, 5	syl 15	. . . . . . . . 9 |- (-. ps -> ((ph /\ ch) <-> ((ph /\ ps) \/ (ph /\ ch))))
7	6	pm5.74i 236	. . . . . . . 8 |- ((-. ps -> (ph /\ ch)) <-> (-. ps -> ((ph /\ ps) \/ (ph /\ ch))))
8		df-or 359	. . . . . . . 8 |- ((ps \/ (ph /\ ch)) <-> (-. ps -> (ph /\ ch)))
9		df-or 359	. . . . . . . 8 |- ((ps \/ ((ph /\ ps) \/ (ph /\ ch))) <-> (-. ps -> ((ph /\ ps) \/ (ph /\ ch))))
10	7, 8, 9	3bitr4i 268	. . . . . . 7 |- ((ps \/ (ph /\ ch)) <-> (ps \/ ((ph /\ ps) \/ (ph /\ ch))))
11		orcom 376	. . . . . . 7 |- (((ph /\ ch) \/ ps) <-> (ps \/ (ph /\ ch)))
12		orcom 376	. . . . . . 7 |- ((((ph /\ ps) \/ (ph /\ ch)) \/ ps) <-> (ps \/ ((ph /\ ps) \/ (ph /\ ch))))
13	10, 11, 12	3bitr4i 268	. . . . . 6 |- (((ph /\ ch) \/ ps) <-> (((ph /\ ps) \/ (ph /\ ch)) \/ ps))
14		orcom 376	. . . . . . 7 |- ((ch \/ ps) <-> (ps \/ ch))
15	14	anbi2i 675	. . . . . 6 |- (((ph \/ ps) /\ (ch \/ ps)) <-> ((ph \/ ps) /\ (ps \/ ch)))
16	2, 13, 15	3bitr3i 266	. . . . 5 |- ((((ph /\ ps) \/ (ph /\ ch)) \/ ps) <-> ((ph \/ ps) /\ (ps \/ ch)))
17		simpr 447	. . . . . . . . . . 11 |- ((ph /\ ch) -> ch)
18	17	con3i 127	. . . . . . . . . 10 |- (-. ch -> -. (ph /\ ch))
19		biorf 394	. . . . . . . . . . 11 |- (-. (ph /\ ch) -> ((ph /\ ps) <-> ((ph /\ ch) \/ (ph /\ ps))))
20		orcom 376	. . . . . . . . . . 11 |- (((ph /\ ch) \/ (ph /\ ps)) <-> ((ph /\ ps) \/ (ph /\ ch)))
21	19, 20	syl6bb 252	. . . . . . . . . 10 |- (-. (ph /\ ch) -> ((ph /\ ps) <-> ((ph /\ ps) \/ (ph /\ ch))))
22	18, 21	syl 15	. . . . . . . . 9 |- (-. ch -> ((ph /\ ps) <-> ((ph /\ ps) \/ (ph /\ ch))))
23	22	pm5.74i 236	. . . . . . . 8 |- ((-. ch -> (ph /\ ps)) <-> (-. ch -> ((ph /\ ps) \/ (ph /\ ch))))
24		df-or 359	. . . . . . . 8 |- ((ch \/ (ph /\ ps)) <-> (-. ch -> (ph /\ ps)))
25		df-or 359	. . . . . . . 8 |- ((ch \/ ((ph /\ ps) \/ (ph /\ ch))) <-> (-. ch -> ((ph /\ ps) \/ (ph /\ ch))))
26	23, 24, 25	3bitr4i 268	. . . . . . 7 |- ((ch \/ (ph /\ ps)) <-> (ch \/ ((ph /\ ps) \/ (ph /\ ch))))
27		orcom 376	. . . . . . 7 |- (((ph /\ ps) \/ ch) <-> (ch \/ (ph /\ ps)))
28		orcom 376	. . . . . . 7 |- ((((ph /\ ps) \/ (ph /\ ch)) \/ ch) <-> (ch \/ ((ph /\ ps) \/ (ph /\ ch))))
29	26, 27, 28	3bitr4i 268	. . . . . 6 |- (((ph /\ ps) \/ ch) <-> (((ph /\ ps) \/ (ph /\ ch)) \/ ch))
30		ordir 835	. . . . . 6 |- (((ph /\ ps) \/ ch) <-> ((ph \/ ch) /\ (ps \/ ch)))
31	29, 30	bitr3i 242	. . . . 5 |- ((((ph /\ ps) \/ (ph /\ ch)) \/ ch) <-> ((ph \/ ch) /\ (ps \/ ch)))
32	16, 31	anbi12i 678	. . . 4 |- (((((ph /\ ps) \/ (ph /\ ch)) \/ ps) /\ (((ph /\ ps) \/ (ph /\ ch)) \/ ch)) <-> (((ph \/ ps) /\ (ps \/ ch)) /\ ((ph \/ ch) /\ (ps \/ ch))))
33	1, 32	bitri 240	. . 3 |- ((((ph /\ ps) \/ (ph /\ ch)) \/ (ps /\ ch)) <-> (((ph \/ ps) /\ (ps \/ ch)) /\ ((ph \/ ch) /\ (ps \/ ch))))
34		df-3or 935	. . 3 |- (((ph /\ ps) \/ (ph /\ ch) \/ (ps /\ ch)) <-> (((ph /\ ps) \/ (ph /\ ch)) \/ (ps /\ ch)))
35		anandir 802	. . 3 |- ((((ph \/ ps) /\ (ph \/ ch)) /\ (ps \/ ch)) <-> (((ph \/ ps) /\ (ps \/ ch)) /\ ((ph \/ ch) /\ (ps \/ ch))))
36	33, 34, 35	3bitr4i 268	. 2 |- (((ph /\ ps) \/ (ph /\ ch) \/ (ps /\ ch)) <-> (((ph \/ ps) /\ (ph \/ ch)) /\ (ps \/ ch)))
37		cador 1391	. 2 |- (cadd(ph, ps, ch) <-> ((ph /\ ps) \/ (ph /\ ch) \/ (ps /\ ch)))
38		df-3an 936	. 2 |- (((ph \/ ps) /\ (ph \/ ch) /\ (ps \/ ch)) <-> (((ph \/ ps) /\ (ph \/ ch)) /\ (ps \/ ch)))
39	36, 37, 38	3bitr4i 268	1 |- (cadd(ph, ps, ch) <-> ((ph \/ ps) /\ (ph \/ ch) /\ (ps \/ ch)))

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   \/ wo 357   /\ wa 358   \/ w3o 933   /\ w3a 934  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-3or 935  df-3an 936  df-xor 1305  df-cad 1381

This theorem is referenced by:  cadnot  1394