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

 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 φ → (hadd(φ, ψ, χ) ↔ (ψχ)))

Proof of Theorem had0
StepHypRef Expression
1 had1 1402 . . 3 φ → (hadd(¬ φ, ¬ ψ, ¬ χ) ↔ (¬ ψ ↔ ¬ χ)))
2 hadnot 1393 . . 3 (¬ hadd(φ, ψ, χ) ↔ hadd(¬ φ, ¬ ψ, ¬ χ))
3 df-xor 1305 . . . . 5 ((¬ ψ ⊻ ¬ χ) ↔ ¬ (¬ ψ ↔ ¬ χ))
4 xorneg 1313 . . . . 5 ((¬ ψ ⊻ ¬ χ) ↔ (ψχ))
53, 4bitr3i 242 . . . 4 (¬ (¬ ψ ↔ ¬ χ) ↔ (ψχ))
65con1bii 321 . . 3 (¬ (ψχ) ↔ (¬ ψ ↔ ¬ χ))
71, 2, 63bitr4g 279 . 2 φ → (¬ hadd(φ, ψ, χ) ↔ ¬ (ψχ)))
87con4bid 284 1 φ → (hadd(φ, ψ, χ) ↔ (ψχ)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ⊻ wxo 1304  haddwhad 1378 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177  df-xor 1305  df-had 1380 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator