Theorem hadnot 1393

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

Assertion

Ref	Expression
hadnot	|- (-. hadd(ph, ps, ch) <-> hadd(-. ph, -. ps, -. ch))

Proof of Theorem hadnot

Step	Hyp	Ref	Expression
1		xorneg 1313	. . . 4 |- ((-. ph \/_ -. ps) <-> (ph \/_ ps))
2		biid 227	. . . 4 |- (-. ch <-> -. ch)
3	1, 2	xorbi12i 1314	. . 3 |- (((-. ph \/_ -. ps) \/_ -. ch) <-> ((ph \/_ ps) \/_ -. ch))
4		xorneg2 1312	. . 3 |- (((ph \/_ ps) \/_ -. ch) <-> -. ((ph \/_ ps) \/_ ch))
5	3, 4	bitr2i 241	. 2 |- (-. ((ph \/_ ps) \/_ ch) <-> ((-. ph \/_ -. ps) \/_ -. ch))
6		df-had 1380	. . 3 |- (hadd(ph, ps, ch) <-> ((ph \/_ ps) \/_ ch))
7	6	notbii 287	. 2 |- (-. hadd(ph, ps, ch) <-> -. ((ph \/_ ps) \/_ ch))
8		df-had 1380	. 2 |- (hadd(-. ph, -. ps, -. ch) <-> ((-. ph \/_ -. ps) \/_ -. ch))
9	5, 7, 8	3bitr4i 268	1 |- (-. hadd(ph, ps, ch) <-> hadd(-. ph, -. ps, -. ch))

Syntax hints:  -. wn 3   <-> wb 176   \/_ wxo 1304  haddwhad 1378

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-xor 1305  df-had 1380

This theorem is referenced by:  had0  1403