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

Theorem cad1 1388
Description: If one parameter is true, the adder carry is true exactly when at least one of the other parameters is true. (Contributed by Mario Carneiro, 8-Sep-2016.)
Assertion
Ref Expression
cad1  |-  ( ch 
->  (cadd ( ph ,  ps ,  ch )  <->  (
ph  \/  ps )
) )

Proof of Theorem cad1
StepHypRef Expression
1 ibar 490 . . . 4  |-  ( ch 
->  ( ( ph  \/_  ps ) 
<->  ( ch  /\  ( ph  \/_  ps ) ) ) )
21bicomd 192 . . 3  |-  ( ch 
->  ( ( ch  /\  ( ph  \/_  ps )
)  <->  ( ph  \/_  ps ) ) )
32orbi2d 682 . 2  |-  ( ch 
->  ( ( ( ph  /\ 
ps )  \/  ( ch  /\  ( ph  \/_  ps ) ) )  <->  ( ( ph  /\  ps )  \/  ( ph  \/_  ps ) ) ) )
4 df-cad 1371 . 2  |-  (cadd (
ph ,  ps ,  ch )  <->  ( ( ph  /\ 
ps )  \/  ( ch  /\  ( ph  \/_  ps ) ) ) )
5 pm5.63 890 . . 3  |-  ( ( ( ph  /\  ps )  \/  ( ph  \/  ps ) )  <->  ( ( ph  /\  ps )  \/  ( -.  ( ph  /\ 
ps )  /\  ( ph  \/  ps ) ) ) )
6 olc 373 . . . 4  |-  ( (
ph  \/  ps )  ->  ( ( ph  /\  ps )  \/  ( ph  \/  ps ) ) )
7 orc 374 . . . . . 6  |-  ( ph  ->  ( ph  \/  ps ) )
87adantr 451 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( ph  \/  ps ) )
9 id 19 . . . . 5  |-  ( (
ph  \/  ps )  ->  ( ph  \/  ps ) )
108, 9jaoi 368 . . . 4  |-  ( ( ( ph  /\  ps )  \/  ( ph  \/  ps ) )  -> 
( ph  \/  ps ) )
116, 10impbii 180 . . 3  |-  ( (
ph  \/  ps )  <->  ( ( ph  /\  ps )  \/  ( ph  \/  ps ) ) )
12 xor2 1301 . . . . 5  |-  ( (
ph  \/_  ps )  <->  ( ( ph  \/  ps )  /\  -.  ( ph  /\ 
ps ) ) )
13 ancom 437 . . . . 5  |-  ( ( ( ph  \/  ps )  /\  -.  ( ph  /\ 
ps ) )  <->  ( -.  ( ph  /\  ps )  /\  ( ph  \/  ps ) ) )
1412, 13bitri 240 . . . 4  |-  ( (
ph  \/_  ps )  <->  ( -.  ( ph  /\  ps )  /\  ( ph  \/  ps ) ) )
1514orbi2i 505 . . 3  |-  ( ( ( ph  /\  ps )  \/  ( ph  \/_ 
ps ) )  <->  ( ( ph  /\  ps )  \/  ( -.  ( ph  /\ 
ps )  /\  ( ph  \/  ps ) ) ) )
165, 11, 153bitr4i 268 . 2  |-  ( (
ph  \/  ps )  <->  ( ( ph  /\  ps )  \/  ( ph  \/_ 
ps ) ) )
173, 4, 163bitr4g 279 1  |-  ( ch 
->  (cadd ( ph ,  ps ,  ch )  <->  (
ph  \/  ps )
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    \/_ wxo 1295  caddwcad 1369
This theorem is referenced by:  sadadd2lem2  12657  sadcaddlem  12664
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-xor 1296  df-cad 1371
  Copyright terms: Public domain W3C validator