cadan - Metamath Proof Explorer

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

Theorem cadan 1434

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 966	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
2		cador 1433	. . . 4 cadd $/\$ $\/$ $/\$ $\/$ $/\$
3		andi 862	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$
4	3	orbi1i 520	. . . 4 $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
5	1, 2, 4	3bitr4i 277	. . 3 cadd $/\$ $\/$ $\/$ $/\$
6		ordir 860	. . 3 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$
7		ordi 859	. . . 4 $\/$ $/\$ $\/$ $/\$ $\/$
8		orcom 387	. . . . 5 $\/$ $\/$ $/\$ $/\$ $\/$ $\/$
9		simpl 457	. . . . . . 7 $/\$
10	9	orcd 392	. . . . . 6 $/\$ $\/$
11		pm4.72 871	. . . . . 6 $/\$ $\/$ $\/$ $/\$ $\/$ $\/$
12	10, 11	mpbi 208	. . . . 5 $\/$ $/\$ $\/$ $\/$
13	8, 12	bitr4i 252	. . . 4 $\/$ $\/$ $/\$ $\/$
14	7, 13	anbi12i 697	. . 3 $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
15	5, 6, 14	3bitri 271	. 2 cadd $\/$ $/\$ $\/$ $/\$ $\/$
16		df-3an 967	. 2 $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$
17	15, 16	bitr4i 252	1 cadd $\/$ $/\$ $\/$ $/\$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $\/$ w3o 964 $/\$ w3a 965 caddwcad 1421

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 370 df-an 371 df-3or 966 df-3an 967 df-xor 1352 df-cad 1423

This theorem is referenced by: cadnot 1437

W3C validator