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

 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

StepHypRef Expression
1 ibar 491 . . . 4
21bicomd 193 . . 3
32orbi2d 683 . 2
5 pm5.63 891 . . 3
6 olc 374 . . . 4
7 orc 375 . . . . . 6
87adantr 452 . . . . 5
9 id 20 . . . . 5
108, 9jaoi 369 . . . 4
116, 10impbii 181 . . 3
12 xor2 1319 . . . . 5
13 ancom 438 . . . . 5
1412, 13bitri 241 . . . 4
1514orbi2i 506 . . 3
165, 11, 153bitr4i 269 . 2
173, 4, 163bitr4g 280 1 cadd
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wo 358   wa 359   wxo 1313  caddwcad 1388 This theorem is referenced by:  sadadd2lem2  12954  sadcaddlem  12961 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 1314  df-cad 1390
 Copyright terms: Public domain W3C validator