cadan - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cadan		Structured version Unicode version

Theorem cadan 1462

Description: Write the adder carry in conjunctive normal form. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 25-Sep-2018.)

**Assertion**
Ref	Expression
cadan	cadd $\/$ $/\$ $\/$ $/\$ $\/$

**Proof of Theorem cadan**
Step	Hyp	Ref	Expression
1		df-3or 972	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
2		cador 1461	. . . 4 cadd $/\$ $\/$ $/\$ $\/$ $/\$
3		andi 865	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$
4	3	orbi1i 518	. . . 4 $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
5	1, 2, 4	3bitr4i 277	. . 3 cadd $/\$ $\/$ $\/$ $/\$
6		ordir 863	. . 3 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$
7		ordi 862	. . . 4 $\/$ $/\$ $\/$ $/\$ $\/$
8		orcom 385	. . . . 5 $\/$ $\/$ $/\$ $/\$ $\/$ $\/$
9		simpl 455	. . . . . . 7 $/\$
10	9	orcd 390	. . . . . 6 $/\$ $\/$
11		pm4.72 874	. . . . . 6 $/\$ $\/$ $\/$ $/\$ $\/$ $\/$
12	10, 11	mpbi 208	. . . . 5 $\/$ $/\$ $\/$ $\/$
13	8, 12	bitr4i 252	. . . 4 $\/$ $\/$ $/\$ $\/$
14	7, 13	anbi12i 695	. . 3 $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
15	5, 6, 14	3bitri 271	. 2 cadd $\/$ $/\$ $\/$ $/\$ $\/$
16		df-3an 973	. 2 $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$
17	15, 16	bitr4i 252	1 cadd $\/$ $/\$ $\/$ $/\$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367 $\/$ w3o 970 $/\$ w3a 971 caddwcad 1449

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 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-xor 1363 df-cad 1451

This theorem is referenced by: cadnot 1464 cad1 1468

W3C validator