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

Theorem cadifp 1622
Description: The value of the carry is, if the input carry is true, the disjunction, and if the input carry is false, the conjunction, of the other two inputs. (Contributed by BJ, 8-Oct-2019.)
Assertion
Ref Expression
cadifp (cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜒, (𝜑𝜓), (𝜑𝜓)))

Proof of Theorem cadifp
StepHypRef Expression
1 cad1 1619 . 2 (𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
2 cad0 1620 . 2 𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
31, 2casesifp 1078 1 (cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜒, (𝜑𝜓), (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  wo 846  if-wif 1062  caddwcad 1608
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ifp 1063  df-3or 1089  df-3an 1090  df-xor 1511  df-cad 1609
This theorem is referenced by:  wl-df-3mintru2  36365
  Copyright terms: Public domain W3C validator