Theorem adantlr 477

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
adantlr	|- ( ( ( ph /\ th ) /\ ps ) -> ch )

Proof of Theorem adantlr

Step	Hyp	Ref	Expression
1		simpl 109	. 2 |- ( ( ph /\ th ) -> ph )
2		adant2.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	sylan 283	1 |- ( ( ( ph /\ th ) /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  ad2antrr  488  ad2ant2r  509  ad2ant2rl  511  adantl3r  512  ad4ant14  514  ad4ant24  516  ad5ant13  519  ad5ant14  520  ad5ant15  521  3ad2antl1  1186  3ad2antl2  1187  ad4ant124  1243  3adant1r  1258  ad5ant235  1265  ad5ant135  1270  bilukdc  1441  elpr2elpr  3879  intab  3977  pofun  4432  ralxfrd  4582  rexxfrd  4583  ordtri2or2exmidlem  4647  wessep  4699  poinxp  4818  relop  4904  fun11iun  5634  ssimaex  5737  fndmdif  5782  fconst2g  5898  foeqcnvco  5962  f1eqcocnv  5963  isocnv  5983  isocnv2  5984  riota2df  6024  caofdig  6299  f1o2ndf1  6423  tfr1onlembacc  6572  tfr1onlemaccex  6578  tfr1onlemres  6579  tfrcllembacc  6585  tfrcllemaccex  6591  tfrcllemres  6592  tfrcldm  6593  tfrcl  6594  xpdom2  7081  fimax2gtrilemstep  7157  xpfi  7191  eqsupti  7286  ordiso2  7325  enumctlemm  7404  enwomnilem  7459  cc2lem  7579  mulcanpig  7649  prarloclemlt  7807  genpdf  7822  genpdisj  7837  addnqprl  7843  addnqpru  7844  addlocpr  7850  prmuloc  7880  mulnqprl  7882  mulnqpru  7883  mullocpr  7885  ltpopr  7909  ltsopr  7910  ltaddpr  7911  ltexprlemdisj  7920  ltexprlemloc  7921  ltexprlemru  7926  addcanprleml  7928  addcanprlemu  7929  ltaprg  7933  recexprlemopu  7941  recexprlemloc  7945  cauappcvgprlemladdfl  7969  cauappcvgprlemladdru  7970  caucvgsrlemcau  8107  caucvgsrlemgt1  8109  caucvgsrlemoffcau  8112  caucvgsrlemoffres  8114  suplocsrlem  8122  axcaucvglemcau  8212  axpre-suploclemres  8215  axsuploc  8345  cnegexlem1  8447  cnegexlem3  8449  cnegex  8450  addsubeq4  8487  rimul  8858  divcanap6  8992  ltmul12a  9133  lemul12b  9134  lbinf  9221  zrevaddcl  9627  nzadd  9629  zextle  9668  fzind  9692  uz11  9876  infregelbex  9929  qreccl  9973  qrevaddcl  9975  irradd  9977  xrlttr  10127  xrltso  10128  xaddass  10201  xleadd1a  10205  xlt2add  10212  iccshftr  10326  iccshftl  10328  iccdil  10330  icccntr  10332  divelunit  10334  uzsubsubfz  10380  fzaddel  10392  fzrev  10417  elfzmlbp  10465  infssuzex  10592  zsupssdc  10597  frec2uzrdg  10770  frecuzrdgtcl  10773  frecuzrdgsuc  10775  frecuzrdgdomlem  10778  frecuzrdgfunlem  10780  frecuzrdgsuctlem  10784  iseqovex  10819  seq3val  10821  seqf  10825  seq3clss  10832  seq3fveq2  10836  seq3feq2  10837  seq3feq  10841  seq3shft2  10842  ser3mono  10848  seq3split  10849  seqsplitg  10850  seq3caopr3  10852  seq3caopr2  10854  seqcaopr2g  10855  iseqf1olemab  10863  seq3f1olemqsumkj  10872  seq3f1olemqsumk  10873  seq3f1olemqsum  10874  seq3f1olemstep  10875  seq3f1oleml  10877  seqf1oglem2a  10879  seqf1oglem2  10881  seq3id3  10885  seq3id  10886  seq3id2  10887  seq3homo  10888  seq3z  10889  seqfeq3  10890  seqhomog  10891  seqfeq4g  10892  ser3ge0  10897  expp1  10907  expnegap0  10908  expcllem  10911  mulexp  10939  expadd  10942  expaddzap  10944  expmulzap  10946  expdivap  10951  leexp1a  10955  expnlbnd  11025  bcpasc  11127  bccl  11128  hashfacen  11204  seq3coll  11210  ccatlen  11279  ccatvalfn  11285  ccatsymb  11286  ccatalpha  11297  pfxclz  11367  wrd2ind  11411  swrdccat  11423  seq3shft  11519  resqrexlemfp1  11690  sqrtdiv  11723  climshftlemg  11983  climcn1  11989  climsqz  12016  climsqz2  12017  clim2ser  12018  clim2ser2  12019  isermulc2  12021  climub  12025  serf0  12033  fsum3cvg  12060  sumrbdc  12061  summodclem3  12062  summodclem2a  12063  zsumdc  12066  fsumf1o  12072  isumss  12073  fisumss  12074  isumss2  12075  fsum3cvg2  12076  fsum3cvg3  12078  fsumcl2lem  12080  fsumcllem  12081  fsumadd  12088  fsumsplit  12089  fsumsplitsn  12092  sumsplitdc  12114  fisumrev2  12128  fsum2mul  12135  fsum00  12144  telfsumo  12148  fsumparts  12152  iserabs  12157  cvgratnnlemabsle  12209  cvgratnn  12213  cvgratz  12214  mertenslemub  12216  mertenslemi1  12217  mertenslem2  12218  mertensabs  12219  clim2prod  12221  clim2divap  12222  prodfap0  12227  prodfrecap  12228  prodeq2  12239  fproddccvg  12254  prodrbdclem2  12255  prodmodc  12260  zproddc  12261  fprodf1o  12270  fprodssdc  12272  fprodunsn  12286  fprodcllem  12288  fprodabs  12298  fprodeq0  12299  fprodmodd  12323  eftlcvg  12369  negdvdsb  12489  dvdsnegb  12490  fsumdvds  12524  dvdsext  12537  addmodlteqALT  12541  nno  12588  gcdsupex  12649  gcdsupcl  12650  bezoutlembz  12696  dvdssq  12723  eucalgf  12748  dvdslcm  12762  lcmledvds  12763  lcmeq0  12764  lcmcl  12765  lcmdvds  12772  lcmgcdeq  12776  divgcdcoprmex  12795  isprm5lem  12834  phibndlem  12909  phiprmpw  12915  pc2dvds  13024  pcmpt  13037  prmpwdvds  13049  1arith  13061  4sqleminfi  13091  ctiunctlemf  13181  ctiunct  13183  grpinva  13591  grprida  13592  gsumpropd2  13598  sgrppropd  13618  prdssgrpd  13620  mndpropd  13645  prdsidlem  13652  prdsmndd  13653  mhmpropd  13671  0mhm  13691  resmhm2  13693  resmhm2b  13694  grplcan  13767  mulgval  13831  mulgnn0z  13858  mulgnndir  13860  mulgnn0dir  13861  issubg2m  13898  issubg4m  13902  subgintm  13907  ghmf1  13982  gsumfzmptfidmadd  14048  gsumfzmhm  14052  srglmhm  14129  srgrmhm  14130  ringpropd  14174  crngpropd  14175  ringlghm  14197  ringrghm  14198  mulgass3  14221  issubrng2  14347  subrngpropd  14353  issubrg2  14378  subrgintm  14380  subrgpropd  14390  rhmpropd  14391  unitrrg  14405  lmodprop2d  14488  islss3  14519  lssintclm  14524  qusrhm  14668  gsumfzfsum  14728  opnssneib  15013  neissex  15022  tgrest  15026  iscnp3  15060  cnpnei  15076  cnrest  15092  tx1cn  15126  txcnp  15128  elbl3ps  15251  elbl3  15252  blininf  15281  blssexps  15286  blssex  15287  blpnfctr  15296  mopni2  15340  blsscls2  15350  metss  15351  bdmet  15359  metrest  15363  metcn  15371  txmetcn  15376  bl2ioo  15407  ivthinclemlr  15494  ivthinclemur  15496  dvcj  15566  dvfre  15567  elplyd  15598  plyaddlem1  15604  plymullem1  15605  plymullem  15607  plycolemc  15615  plycjlemc  15617  coseq0q4123  15691  abssinper  15703  fsumdvdsmul  15851  lgsval2lem  15875  lgsval4lem  15876  lgsneg  15889  lgsmod  15891  lgsdir2  15898  lgsdir  15900  lgsne0  15903  lgssq  15905  lgsquadlem1  15942  usgredg2vlem2  16210  clwwlkccat  16388  clwwlknonex2lem2  16425  subctctexmid  16766  cvgcmp2n  16809  iswomninnlem  16826  nconstwlpo  16843