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

Theorem cador 1458
Description: Write the adder carry in disjunctive normal form. (Contributed by Mario Carneiro, 4-Sep-2016.)
Assertion
Ref Expression
cador

Proof of Theorem cador
StepHypRef Expression
1 df-cad 1448 . 2
2 xor2 1369 . . . . . . 7
32rbaib 906 . . . . . 6
43anbi1d 704 . . . . 5
5 ancom 450 . . . . 5
6 andir 868 . . . . 5
74, 5, 63bitr3g 287 . . . 4
87pm5.74i 245 . . 3
9 df-or 370 . . 3
10 3orass 976 . . . 4
11 df-or 370 . . . 4
1210, 11bitri 249 . . 3
138, 9, 123bitr4i 277 . 2
141, 13bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  \/w3o 972  \/_wxo 1363  caddwcad 1446
This theorem is referenced by:  cadan  1459  cadnot  1461  cadcomb  1463
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 185  df-or 370  df-an 371  df-3or 974  df-xor 1364  df-cad 1448
  Copyright terms: Public domain W3C validator