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

Theorem cadifp 1516
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 (
ph ,  ps ,  ch )  <-> if- ( ch ,  (
ph  \/  ps ) ,  ( ph  /\  ps ) ) )

Proof of Theorem cadifp
StepHypRef Expression
1 cad1 1514 . 2  |-  ( ch 
->  (cadd ( ph ,  ps ,  ch )  <->  (
ph  \/  ps )
) )
2 cad0 1515 . 2  |-  ( -. 
ch  ->  (cadd ( ph ,  ps ,  ch )  <->  (
ph  /\  ps )
) )
31, 2casesifp 1434 1  |-  (cadd (
ph ,  ps ,  ch )  <-> if- ( ch ,  (
ph  \/  ps ) ,  ( ph  /\  ps ) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    \/ wo 369    /\ wa 370  if-wif 1420  caddwcad 1504
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 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-xor 1401  df-ifp 1421  df-cad 1505
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator