cadnot - Metamath Proof Explorer

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

Theorem cadnot 1554

Description: The adder carry distributes over negation. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 11-Jul-2020.)

**Assertion**
Ref	Expression
cadnot	cadd cadd

**Proof of Theorem cadnot**
Step	Hyp	Ref	Expression
1		ianor 509	. . 3 $/\$ $\/$
2		ianor 509	. . 3 $/\$ $\/$
3		ianor 509	. . 3 $/\$ $\/$
4	1, 2, 3	3anbi123i 1251	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
5		3ioran 1056	. . 3 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
6		cador 1547	. . 3 cadd $/\$ $\/$ $/\$ $\/$ $/\$
7	5, 6	xchnxbir 323	. 2 cadd $/\$ $/\$ $/\$ $/\$ $/\$
8		cadan 1548	. 2 cadd $\/$ $/\$ $\/$ $/\$ $\/$
9	4, 7, 8	3bitr4i 292	1 cadd cadd

Colors of variables: wff setvar class

Syntax hints:

wn 3

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: (None)

W3C validator