cadnot - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > cadnot		Unicode version

Theorem cadnot 1394

Description: The adder carry distributes over negation. (Contributed by Mario Carneiro, 4-Sep-2016.)

**Assertion**
Ref	Expression
cadnot	cadd cadd

**Proof of Theorem cadnot**
Step	Hyp	Ref	Expression
1		3ioran 950	. . 3 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
2		ianor 474	. . . 4 $/\$ $\/$
3		ianor 474	. . . 4 $/\$ $\/$
4		ianor 474	. . . 4 $/\$ $\/$
5	2, 3, 4	3anbi123i 1140	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
6	1, 5	bitri 240	. 2 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
7		cador 1391	. . 3 cadd $/\$ $\/$ $/\$ $\/$ $/\$
8	7	notbii 287	. 2 cadd $/\$ $\/$ $/\$ $\/$ $/\$
9		cadan 1392	. 2 cadd $\/$ $/\$ $\/$ $/\$ $\/$
10	6, 8, 9	3bitr4i 268	1 cadd cadd

Colors of variables: wff setvar class

Syntax hints:

wn 3

wb 176 $\/$ wo 357 $/\$ wa 358 $\/$ w3o 933 $/\$ w3a 934 caddwcad 1379

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 177 df-or 359 df-an 360 df-3or 935 df-3an 936 df-xor 1305 df-cad 1381

This theorem is referenced by: (None)