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

Theorem cad1 1404
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 491 . . . 4  |-  ( ch 
->  ( ( ph  \/_  ps ) 
<->  ( ch  /\  ( ph  \/_  ps ) ) ) )
21bicomd 193 . . 3  |-  ( ch 
->  ( ( ch  /\  ( ph  \/_  ps )
)  <->  ( ph  \/_  ps ) ) )
32orbi2d 683 . 2  |-  ( ch 
->  ( ( ( ph  /\ 
ps )  \/  ( ch  /\  ( ph  \/_  ps ) ) )  <->  ( ( ph  /\  ps )  \/  ( ph  \/_  ps ) ) ) )
4 df-cad 1387 . 2  |-  (cadd (
ph ,  ps ,  ch )  <->  ( ( ph  /\ 
ps )  \/  ( ch  /\  ( ph  \/_  ps ) ) ) )
5 pm5.63 891 . . 3  |-  ( ( ( ph  /\  ps )  \/  ( ph  \/  ps ) )  <->  ( ( ph  /\  ps )  \/  ( -.  ( ph  /\ 
ps )  /\  ( ph  \/  ps ) ) ) )
6 olc 374 . . . 4  |-  ( (
ph  \/  ps )  ->  ( ( ph  /\  ps )  \/  ( ph  \/  ps ) ) )
7 orc 375 . . . . . 6  |-  ( ph  ->  ( ph  \/  ps ) )
87adantr 452 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( ph  \/  ps ) )
9 id 20 . . . . 5  |-  ( (
ph  \/  ps )  ->  ( ph  \/  ps ) )
108, 9jaoi 369 . . . 4  |-  ( ( ( ph  /\  ps )  \/  ( ph  \/  ps ) )  -> 
( ph  \/  ps ) )
116, 10impbii 181 . . 3  |-  ( (
ph  \/  ps )  <->  ( ( ph  /\  ps )  \/  ( ph  \/  ps ) ) )
12 xor2 1316 . . . . 5  |-  ( (
ph  \/_  ps )  <->  ( ( ph  \/  ps )  /\  -.  ( ph  /\ 
ps ) ) )
13 ancom 438 . . . . 5  |-  ( ( ( ph  \/  ps )  /\  -.  ( ph  /\ 
ps ) )  <->  ( -.  ( ph  /\  ps )  /\  ( ph  \/  ps ) ) )
1412, 13bitri 241 . . . 4  |-  ( (
ph  \/_  ps )  <->  ( -.  ( ph  /\  ps )  /\  ( ph  \/  ps ) ) )
1514orbi2i 506 . . 3  |-  ( ( ( ph  /\  ps )  \/  ( ph  \/_ 
ps ) )  <->  ( ( ph  /\  ps )  \/  ( -.  ( ph  /\ 
ps )  /\  ( ph  \/  ps ) ) ) )
165, 11, 153bitr4i 269 . 2  |-  ( (
ph  \/  ps )  <->  ( ( ph  /\  ps )  \/  ( ph  \/_ 
ps ) ) )
173, 4, 163bitr4g 280 1  |-  ( ch 
->  (cadd ( ph ,  ps ,  ch )  <->  (
ph  \/  ps )
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    \/_ wxo 1310  caddwcad 1385
This theorem is referenced by:  sadadd2lem2  12889  sadcaddlem  12896
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 178  df-or 360  df-an 361  df-xor 1311  df-cad 1387
  Copyright terms: Public domain W3C validator