MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-had Structured version   Visualization version   GIF version

Definition df-had 1532
Description: Definition of the "sum" output of the full adder (triple exclusive disjunction, or XOR3). (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 1531 . 2 wff hadd(𝜑, 𝜓, 𝜒)
51, 2wxo 1463 . . 3 wff (𝜑𝜓)
65, 3wxo 1463 . 2 wff ((𝜑𝜓) ⊻ 𝜒)
74, 6wb 196 1 wff (hadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ⊻ 𝜒))
Colors of variables: wff setvar class
This definition is referenced by:  hadbi123d  1533  hadass  1535  hadbi  1536  hadcoma  1537
  Copyright terms: Public domain W3C validator