Theorem cadan 1392

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

Assertion

Ref	Expression
cadan	⊢ (cadd(φ, ψ, χ) ↔ ((φ ∨ ψ) ∧ (φ ∨ χ) ∧ (ψ ∨ χ)))

Proof of Theorem cadan

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358   ∨ w3o 933   ∧ w3a 934  caddwcad 1379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof 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 used by:  cadnot  1394