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

Theorem 3adantl2 1153
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
Hypothesis
Ref Expression
3adantl.1
Assertion
Ref Expression
3adantl2

Proof of Theorem 3adantl2
StepHypRef Expression
1 3simpb 994 . 2
2 3adantl.1 . 2
31, 2sylan 471 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  3ad2antl1  1158  omord2  7235  nnmord  7300  axcc3  8839  lediv2a  10464  zdiv  10958  clatleglb  15756  mulgnn0subcl  16155  mulgsubcl  16156  ghmmulg  16279  obs2ss  18760  scmatf1  19033  neiint  19605  cnpnei  19765  caublcls  21747  axlowdimlem16  24260  clwwlkext2edg  24802  ipval2lem2  25614  ipval2lem5  25620  fh1  26536  cm2j  26538  hoadddi  26722  hoadddir  26723  stoweidlem44  31826  fourierdlem41  31930  fourierdlem42  31931  fourierdlem54  31943  fourierdlem83  31972  lautco  35821
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-an 371  df-3an 975
  Copyright terms: Public domain W3C validator