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

Definition df-cad 1586
Description: Definition of the "carry" output of the full adder. It is true when at least two arguments are true, so it is equal to the "majority" function on three variables. See cador 1587 and cadan 1588 for alternate definitions. (Contributed by Mario Carneiro, 4-Sep-2016.)
Assertion
Ref Expression
df-cad (cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∨ (𝜒 ∧ (𝜑𝜓))))

Detailed syntax breakdown of Definition df-cad
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
3 wch . . 3 wff 𝜒
41, 2, 3wcad 1585 . 2 wff cadd(𝜑, 𝜓, 𝜒)
51, 2wa 383 . . 3 wff (𝜑𝜓)
61, 2wxo 1504 . . . 4 wff (𝜑𝜓)
73, 6wa 383 . . 3 wff (𝜒 ∧ (𝜑𝜓))
85, 7wo 382 . 2 wff ((𝜑𝜓) ∨ (𝜒 ∧ (𝜑𝜓)))
94, 8wb 196 1 wff (cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∨ (𝜒 ∧ (𝜑𝜓))))
Colors of variables: wff setvar class
This definition is referenced by:  cador  1587  cadbi123d  1589  cadcoma  1591  cad0  1596  cad11  1598
  Copyright terms: Public domain W3C validator