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

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

Proof of Theorem 3adantl3
StepHypRef Expression
1 3simpa 993 . 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:  dif1enOLD  7772  dif1en  7773  infpssrlem4  8707  fin23lem11  8718  tskwun  9183  gruf  9210  lediv2a  10464  prunioo  11678  rpnnen2lem7  13954  muldvds1  14008  muldvds2  14009  dvdscmul  14010  dvdsmulc  14011  rpexp  14261  pospropd  15764  mdetmul  19125  elcls  19574  iscnp4  19764  cnpnei  19765  cnpflf2  20501  cnpflf  20502  cnpfcf  20542  xbln0  20917  blcls  21009  iimulcl  21437  icccvx  21450  iscau2  21716  rrxcph  21824  cncombf  22065  mumul  23455  ax5seglem1  24231  ax5seglem2  24232  wwlkext2clwwlk  24803  nvmul0or  25547  fh1  26536  fh2  26537  cm2j  26538  pjoi0  26635  hoadddi  26722  hmopco  26942  iocinif  27592  volfiniune  28202  eulerpartlemb  28307  cnambfre  30063  ivthALT  30153  rngohomco  30377  rngoisoco  30385  lptre2pt  31646  dvnprodlem1  31743  ibliccsinexp  31749  iblioosinexp  31751  fourierdlem12  31901  fourierdlem41  31930  fourierdlem42  31931  fourierdlem48  31937  fourierdlem49  31938  fourierdlem51  31940  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem97  31986  etransclem24  32041  lincdifsn  33025  pexmidlem3N  35696  hdmapglem7  37659
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