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

Theorem adantllr 730
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
Hypothesis
Ref Expression
adantl2.1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
adantllr  |-  ( ( ( ( ph  /\  ta )  /\  ps )  /\  ch )  ->  th )

Proof of Theorem adantllr
StepHypRef Expression
1 simpl 463 . 2  |-  ( (
ph  /\  ta )  ->  ph )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl1 660 1  |-  ( ( ( ( ph  /\  ta )  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  adantl3r  761  r19.29an  2899  elsnxp  5357  oewordri  7280  marypha1lem  7934  gruwun  9225  lemul12b  10451  rlimsqzlem  13723  fsumrlim  13882  fsumo1  13883  lcmdvds  14584  isacs2  15570  tgcl  19996  neindisj  20144  neiptoptop  20158  isr0  20763  cnextcn  21093  ustuqtop4  21270  metss  21534  mbfsup  22632  itg2i1fseqle  22724  ditgsplit  22828  itgulm  23375  leibpi  23880  dchrisumlem3  24341  iscgrglt  24571  legov  24642  legov2  24643  legtrid  24648  colopp  24823  f1otrg  24913  cusgrasize2inds  25217  grpoidinvlem3  25946  grpoideu  25949  grporcan  25961  isgrp2d  25975  blocni  26458  normcan  27241  unoplin  27585  hmoplin  27607  nmophmi  27696  mdslmd3i  27997  chirredlem1  28055  chirredlem2  28056  mdsymlem5  28072  cdj1i  28098  fpwrelmap  28326  archiabllem1  28517  archiabl  28522  isarchiofld  28587  locfinreflem  28674  pstmxmet  28707  ordtconlem1  28737  esumcvg  28914  esum2d  28921  esumiun  28922  ldgenpisyslem1  28992  omssubadd  29134  omssubaddOLD  29138  signstfvneq0  29467  elicc3  30979  poimirlem17  31959  poimirlem20  31962  poimirlem27  31969  poimirlem29  31971  poimir  31975  heicant  31977  itg2addnclem  31995  ftc1anclem5  32023  ftc1anclem6  32024  ftc1anclem7  32025  ftc1anclem8  32026  ftc1anc  32027  fzmul  32071  fdc  32076  fdc1  32077  incsequz2  32080  rrncmslem  32166  ghomco  32183  rngoisocnv  32222  ispridlc  32305  cvgdvgrat  36663  binomcxplemnotnn0  36706  founiiun0  37475  supxrge  37592  suplesup  37593  lptre2pt  37762  0ellimcdiv  37772  limclner  37774  icccncfext  37807  cncfiooiccre  37815  fperdvper  37832  dvnprodlem2  37864  iblcncfioo  37897  stoweidlem35  37953  wallispilem3  37986  fourierdlem20  38046  fourierdlem34  38061  fourierdlem39  38066  fourierdlem42  38069  fourierdlem42OLD  38070  fourierdlem46  38073  fourierdlem48  38075  fourierdlem49  38076  fourierdlem63  38090  fourierdlem64  38091  fourierdlem73  38100  fourierdlem87  38114  fourierdlem97  38124  fourierdlem103  38130  fourierdlem104  38131  fourierdlem111  38138  etransclem32  38188  etransclem33  38189  etransclem35  38191  sge0cl  38282  sge0f1o  38283  sge0split  38310  sge0iunmptlemre  38316  sge0rpcpnf  38322  sge0xadd  38336  nnfoctbdjlem  38354  ismeannd  38366  omeiunltfirp  38404  hoidmvlelem3  38482  hoidmvle  38485  ovncvr2  38496  hspdifhsp  38501  hspmbllem2  38512  ovnsubadd2lem  38530  cusgrsize2inds  39616  aacllem  40865
  Copyright terms: Public domain W3C validator