Theorem adantllr 755

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

Step	Hyp	Ref	Expression
1		simpl 473	. 2 |- ( ( ph /\ ta ) -> ph )
2		adantl2.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylanl1 682	1 |- ( ( ( ( ph /\ ta ) /\ ps ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  adantl3r  786  r19.29an  3077  elsnxpOLD  5678  oewordri  7672  marypha1lem  8339  gruwun  9635  lemul12b  10880  rlimsqzlem  14379  fsumrlim  14543  fsumo1  14544  lcmdvds  15321  isacs2  16314  dfgrp3lem  17513  tgcl  20773  neindisj  20921  neiptoptop  20935  isr0  21540  cnextcn  21871  ustuqtop4  22048  metss  22313  mbfsup  23431  itg2i1fseqle  23521  ditgsplit  23625  itgulm  24162  leibpi  24669  dchrisumlem3  25180  iscgrglt  25409  legov  25480  legov2  25481  legtrid  25486  colopp  25661  f1otrg  25751  cusgrsize2inds  26349  grpoidinvlem3  27360  grpoideu  27363  grporcan  27372  blocni  27660  normcan  28435  unoplin  28779  hmoplin  28801  nmophmi  28890  mdslmd3i  29191  chirredlem1  29249  chirredlem2  29250  mdsymlem5  29266  cdj1i  29292  fpwrelmap  29508  fsumiunle  29575  archiabllem1  29747  archiabl  29752  isarchiofld  29817  locfinreflem  29907  pstmxmet  29940  ordtconnlem1  29970  esumcvg  30148  esum2d  30155  esumiun  30156  ldgenpisyslem1  30226  omssubadd  30362  signstfvneq0  30649  circlemeth  30718  elicc3  32311  knoppcnlem9  32491  lindsenlbs  33404  matunitlindflem1  33405  poimirlem17  33426  poimirlem20  33429  poimirlem27  33436  poimirlem29  33438  poimir  33442  heicant  33444  itg2addnclem  33461  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  fzmul  33537  fdc  33541  fdc1  33542  incsequz2  33545  rrncmslem  33631  ghomco  33690  rngoisocnv  33780  ispridlc  33869  cvgdvgrat  38512  binomcxplemnotnn0  38555  founiiun0  39377  supxrge  39554  suplesup  39555  supxrunb3  39623  lptre2pt  39872  0ellimcdiv  39881  limclner  39883  limsuppnfdlem  39933  limsuppnflem  39942  limsupmnflem  39952  liminfreuzlem  40034  liminflimsupclim  40039  cnrefiisplem  40055  climxlim2lem  40071  icccncfext  40100  cncfiooiccre  40108  fperdvper  40133  dvnprodlem2  40162  iblcncfioo  40194  stoweidlem35  40252  wallispilem3  40284  fourierdlem20  40344  fourierdlem34  40358  fourierdlem39  40363  fourierdlem42  40366  fourierdlem46  40369  fourierdlem48  40371  fourierdlem49  40372  fourierdlem63  40386  fourierdlem64  40387  fourierdlem73  40396  fourierdlem87  40410  fourierdlem97  40420  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  etransclem32  40483  etransclem33  40484  etransclem35  40486  sge0cl  40598  sge0f1o  40599  sge0split  40626  sge0iunmptlemre  40632  sge0rpcpnf  40638  sge0xadd  40652  nnfoctbdjlem  40672  ismeannd  40684  omeiunltfirp  40733  hoidmvlelem3  40811  hoidmvle  40814  ovncvr2  40825  hspdifhsp  40830  hspmbllem2  40841  ovnsubadd2lem  40859  pimdecfgtioo  40927  pimincfltioo  40928  smflimlem1  40979  smflimmpt  41016  aacllem  42547