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

Theorem cadifp 1618
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 1077 1 (cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜒, (𝜑𝜓), (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wo 847  if-wif 1062  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 207  df-an 396  df-or 848  df-ifp 1063  df-3or 1087  df-3an 1088  df-xor 1511  df-cad 1606
This theorem is referenced by:  wl-df-3mintru2  37486
  Copyright terms: Public domain W3C validator