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

Theorem cadifp 1554
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 1552 . 2 (𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
2 cad0 1553 . 2 𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
31, 2casesifp 1025 1 (cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜒, (𝜑𝜓), (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wo 383  wa 384  if-wif 1011  caddwcad 1542
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 197  df-or 385  df-an 386  df-ifp 1012  df-3or 1037  df-3an 1038  df-xor 1462  df-cad 1543
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator