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

Theorem cadifp 1619
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 1616 . 2 (𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
2 cad0 1617 . 2 𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
31, 2casesifp 1075 1 (cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜒, (𝜑𝜓), (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  wo 843  if-wif 1059  caddwcad 1605
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 395  df-or 844  df-ifp 1060  df-3or 1086  df-3an 1087  df-xor 1508  df-cad 1606
This theorem is referenced by:  wl-df-3mintru2  36668
  Copyright terms: Public domain W3C validator