Theorem had0 1403

Description: If the first parameter is false, the half adder is equivalent to the XOR of the other two inputs. (Contributed by Mario Carneiro, 4-Sep-2016.)

Assertion

Ref	Expression
had0	|- (-. ph -> (hadd(ph, ps, ch) <-> (ps \/_ ch)))

Proof of Theorem had0

Step	Hyp	Ref	Expression
1		had1 1402	. . 3 |- (-. ph -> (hadd(-. ph, -. ps, -. ch) <-> (-. ps <-> -. ch)))
2		hadnot 1393	. . 3 |- (-. hadd(ph, ps, ch) <-> hadd(-. ph, -. ps, -. ch))
3		df-xor 1305	. . . . 5 |- ((-. ps \/_ -. ch) <-> -. (-. ps <-> -. ch))
4		xorneg 1313	. . . . 5 |- ((-. ps \/_ -. ch) <-> (ps \/_ ch))
5	3, 4	bitr3i 242	. . . 4 |- (-. (-. ps <-> -. ch) <-> (ps \/_ ch))
6	5	con1bii 321	. . 3 |- (-. (ps \/_ ch) <-> (-. ps <-> -. ch))
7	1, 2, 6	3bitr4g 279	. 2 |- (-. ph -> (-. hadd(ph, ps, ch) <-> -. (ps \/_ ch)))
8	7	con4bid 284	1 |- (-. ph -> (hadd(ph, ps, ch) <-> (ps \/_ ch)))

Syntax hints:  -. wn 3   -> wi 4   <-> 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: (None)