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

Theorem cad11 1466
Description: If two parameters are true, the adder carry is true. (Contributed by Mario Carneiro, 4-Sep-2016.)
Assertion
Ref Expression
cad11

Proof of Theorem cad11
StepHypRef Expression
1 orc 385 . 2
2 df-cad 1448 . 2
31, 2sylibr 212 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/wo 368  /\wa 369  \/_wxo 1363  caddwcad 1446
This theorem is referenced by:  cadtru  1469
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-cad 1448
  Copyright terms: Public domain W3C validator