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

Theorem adantllr 723
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 458 . 2  |-  ( (
ph  /\  ta )  ->  ph )
2 adantl2.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylanl1 654 1  |-  ( ( ( ( ph  /\  ta )  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  adantl3r  754  r19.29an  2966  elsnxp  5397  oewordri  7304  marypha1lem  7956  gruwun  9245  lemul12b  10469  rlimsqzlem  13711  fsumrlim  13870  fsumo1  13871  lcmdvds  14572  isacs2  15558  tgcl  19983  neindisj  20131  neiptoptop  20145  isr0  20750  cnextcn  21080  ustuqtop4  21257  metss  21521  mbfsup  22618  itg2i1fseqle  22710  ditgsplit  22814  itgulm  23361  leibpi  23866  dchrisumlem3  24327  iscgrglt  24557  legov  24628  legov2  24629  legtrid  24634  colopp  24809  f1otrg  24899  cusgrasize2inds  25203  grpoidinvlem3  25932  grpoideu  25935  grporcan  25947  isgrp2d  25961  blocni  26444  normcan  27227  unoplin  27571  hmoplin  27593  nmophmi  27682  mdslmd3i  27983  chirredlem1  28041  chirredlem2  28042  mdsymlem5  28058  cdj1i  28084  fpwrelmap  28324  archiabllem1  28517  archiabl  28522  isarchiofld  28588  locfinreflem  28675  pstmxmet  28708  ordtconlem1  28738  esumcvg  28915  esum2d  28922  esumiun  28923  ldgenpisyslem1  28993  omssubadd  29136  omssubaddOLD  29140  signstfvneq0  29469  elicc3  30978  poimirlem17  31921  poimirlem20  31924  poimirlem27  31931  poimirlem29  31933  poimir  31937  heicant  31939  itg2addnclem  31957  ftc1anclem5  31985  ftc1anclem6  31986  ftc1anclem7  31987  ftc1anclem8  31988  ftc1anc  31989  fzmul  32033  fdc  32038  fdc1  32039  incsequz2  32042  rrncmslem  32128  ghomco  32145  rngoisocnv  32184  ispridlc  32267  cvgdvgrat  36632  binomcxplemnotnn0  36675  founiiun0  37426  supxrge  37515  suplesup  37516  lptre2pt  37660  0ellimcdiv  37670  limclner  37672  icccncfext  37705  cncfiooiccre  37713  fperdvper  37730  dvnprodlem2  37762  iblcncfioo  37795  stoweidlem35  37836  wallispilem3  37869  fourierdlem20  37929  fourierdlem34  37944  fourierdlem39  37949  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem46  37956  fourierdlem48  37958  fourierdlem49  37959  fourierdlem63  37973  fourierdlem64  37974  fourierdlem73  37983  fourierdlem87  37997  fourierdlem97  38007  fourierdlem103  38013  fourierdlem104  38014  fourierdlem111  38021  etransclem32  38071  etransclem33  38072  etransclem35  38074  sge0cl  38131  sge0f1o  38132  sge0split  38159  sge0iunmptlemre  38165  sge0rpcpnf  38171  sge0xadd  38185  nnfoctbdjlem  38201  ismeannd  38213  omeiunltfirp  38248  hoidmvlelem3  38323  hoidmvle  38326  cusgrsize2inds  39270  aacllem  40161
  Copyright terms: Public domain W3C validator