cador - Metamath Proof Explorer

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

Theorem cador 1547

Description: The adder carry in disjunctive normal form. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 11-Jul-2020.)

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

**Proof of Theorem cador**
Step	Hyp	Ref	Expression
1		xor2 1470	. . . . . . 7 $\/_$ $\/$ $/\$ $/\$
2	1	rbaib 947	. . . . . 6 $/\$ $\/_$ $\/$
3	2	anbi1d 741	. . . . 5 $/\$ $\/_$ $/\$ $\/$ $/\$
4		ancom 466	. . . . 5 $\/_$ $/\$ $/\$ $\/_$
5		andir 912	. . . . 5 $\/$ $/\$ $/\$ $\/$ $/\$
6	3, 4, 5	3bitr3g 302	. . . 4 $/\$ $/\$ $\/_$ $/\$ $\/$ $/\$
7	6	pm5.74i 260	. . 3 $/\$ $/\$ $\/_$ $/\$ $/\$ $\/$ $/\$
8		df-or 385	. . 3 $/\$ $\/$ $/\$ $\/_$ $/\$ $/\$ $\/_$
9		df-or 385	. . 3 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
10	7, 8, 9	3bitr4i 292	. 2 $/\$ $\/$ $/\$ $\/_$ $/\$ $\/$ $/\$ $\/$ $/\$
11		df-cad 1546	. 2 cadd $/\$ $\/$ $/\$ $\/_$
12		3orass 1040	. 2 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
13	10, 11, 12	3bitr4i 292	1 cadd $/\$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $\/$ w3o 1036 $\/_$ wxo 1464 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-xor 1465 df-cad 1546

This theorem is referenced by: cadan 1548 cadnot 1554

W3C validator