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

Theorem cadifp 1626
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 1623 . 2 (𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
2 cad0 1624 . 2 𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
31, 2casesifp 1076 1 (cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜒, (𝜑𝜓), (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396  wo 844  if-wif 1060  caddwcad 1612
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 397  df-or 845  df-ifp 1061  df-3or 1087  df-3an 1088  df-xor 1507  df-cad 1613
This theorem is referenced by:  wl-df-3mintru2  35643
  Copyright terms: Public domain W3C validator