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 1587
Description: Definition of the "sum" output of the full adder (triple exclusive disjunction, or XOR3, or testing whether an odd number of parameters are true). (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 1586 . 2 wff hadd(𝜑, 𝜓, 𝜒)
51, 2wxo 1497 . . 3 wff (𝜑𝜓)
65, 3wxo 1497 . 2 wff ((𝜑𝜓) ⊻ 𝜒)
74, 6wb 207 1 wff (hadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ⊻ 𝜒))
Colors of variables: wff setvar class
This definition is referenced by:  hadbi123d  1588  hadass  1590  hadbi  1591  hadcomaOLD  1593
  Copyright terms: Public domain W3C validator