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

Definition df-had 1380
Description: Define the half adder (triple XOR). (Contributed by Mario Carneiro, 4-Sep-2016.)
Assertion
Ref Expression
df-had (hadd(φ, ψ, χ) ↔ ((φψ) ⊻ χ))

Detailed syntax breakdown of Definition df-had
StepHypRef Expression
1 wph . . 3 wff φ
2 wps . . 3 wff ψ
3 wch . . 3 wff χ
41, 2, 3whad 1378 . 2 wff hadd(φ, ψ, χ)
51, 2wxo 1304 . . 3 wff (φψ)
65, 3wxo 1304 . 2 wff ((φψ) ⊻ χ)
74, 6wb 176 1 wff (hadd(φ, ψ, χ) ↔ ((φψ) ⊻ χ))
Colors of variables: wff setvar class
This definition is referenced by:  hadbi123d  1382  hadass  1386  hadbi  1387  hadcoma  1388  hadnot  1393
  Copyright terms: Public domain W3C validator