cadan - Metamath Proof Explorer

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

Theorem cadan 1548

Description: 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 1038	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
2		cador 1547	. . . 4 cadd $/\$ $\/$ $/\$ $\/$ $/\$
3		andi 911	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$
4	3	orbi1i 542	. . . 4 $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
5	1, 2, 4	3bitr4i 292	. . 3 cadd $/\$ $\/$ $\/$ $/\$
6		ordir 909	. . 3 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$
7		ordi 908	. . . 4 $\/$ $/\$ $\/$ $/\$ $\/$
8		orcom 402	. . . . 5 $\/$ $\/$ $/\$ $/\$ $\/$ $\/$
9		animorl 505	. . . . . 6 $/\$ $\/$
10		pm4.72 920	. . . . . 6 $/\$ $\/$ $\/$ $/\$ $\/$ $\/$
11	9, 10	mpbi 220	. . . . 5 $\/$ $/\$ $\/$ $\/$
12	8, 11	bitr4i 267	. . . 4 $\/$ $\/$ $/\$ $\/$
13	7, 12	anbi12i 733	. . 3 $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
14	5, 6, 13	3bitri 286	. 2 cadd $\/$ $/\$ $\/$ $/\$ $\/$
15		df-3an 1039	. 2 $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$
16	14, 15	bitr4i 267	1 cadd $\/$ $/\$ $\/$ $/\$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $\/$ w3o 1036 $/\$ w3a 1037 caddwcad 1545

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 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-xor 1465 df-cad 1546

This theorem is referenced by: cadcomb 1552 cadnot 1554 cad1 1555

W3C validator