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  1161  3ad2antl2  1162  ad4ant124  1218  3adant1r  1233  ad5ant235  1240  ad5ant135  1245  bilukdc  1407  intab  3904  pofun  4348  ralxfrd  4498  rexxfrd  4499  ordtri2or2exmidlem  4563  wessep  4615  poinxp  4733  relop  4817  fun11iun  5528  ssimaex  5625  fndmdif  5670  fconst2g  5780  foeqcnvco  5840  f1eqcocnv  5841  isocnv  5861  isocnv2  5862  riota2df  5901  caofdig  6173  f1o2ndf1  6295  tfr1onlembacc  6409  tfr1onlemaccex  6415  tfr1onlemres  6416  tfrcllembacc  6422  tfrcllemaccex  6428  tfrcllemres  6429  tfrcldm  6430  tfrcl  6431  xpdom2  6899  fimax2gtrilemstep  6970  xpfi  7002  eqsupti  7071  ordiso2  7110  enumctlemm  7189  enwomnilem  7244  cc2lem  7349  mulcanpig  7419  prarloclemlt  7577  genpdf  7592  genpdisj  7607  addnqprl  7613  addnqpru  7614  addlocpr  7620  prmuloc  7650  mulnqprl  7652  mulnqpru  7653  mullocpr  7655  ltpopr  7679  ltsopr  7680  ltaddpr  7681  ltexprlemdisj  7690  ltexprlemloc  7691  ltexprlemru  7696  addcanprleml  7698  addcanprlemu  7699  ltaprg  7703  recexprlemopu  7711  recexprlemloc  7715  cauappcvgprlemladdfl  7739  cauappcvgprlemladdru  7740  caucvgsrlemcau  7877  caucvgsrlemgt1  7879  caucvgsrlemoffcau  7882  caucvgsrlemoffres  7884  suplocsrlem  7892  axcaucvglemcau  7982  axpre-suploclemres  7985  axsuploc  8116  cnegexlem1  8218  cnegexlem3  8220  cnegex  8221  addsubeq4  8258  rimul  8629  divcanap6  8763  ltmul12a  8904  lemul12b  8905  lbinf  8992  zrevaddcl  9393  nzadd  9395  zextle  9434  fzind  9458  uz11  9641  infregelbex  9689  qreccl  9733  qrevaddcl  9735  irradd  9737  xrlttr  9887  xrltso  9888  xaddass  9961  xleadd1a  9965  xlt2add  9972  iccshftr  10086  iccshftl  10088  iccdil  10090  icccntr  10092  divelunit  10094  uzsubsubfz  10139  fzaddel  10151  fzrev  10176  elfzmlbp  10224  infssuzex  10340  zsupssdc  10345  frec2uzrdg  10518  frecuzrdgtcl  10521  frecuzrdgsuc  10523  frecuzrdgdomlem  10526  frecuzrdgfunlem  10528  frecuzrdgsuctlem  10532  iseqovex  10567  seq3val  10569  seqf  10573  seq3clss  10580  seq3fveq2  10584  seq3feq2  10585  seq3feq  10589  seq3shft2  10590  ser3mono  10596  seq3split  10597  seqsplitg  10598  seq3caopr3  10600  seq3caopr2  10602  seqcaopr2g  10603  iseqf1olemab  10611  seq3f1olemqsumkj  10620  seq3f1olemqsumk  10621  seq3f1olemqsum  10622  seq3f1olemstep  10623  seq3f1oleml  10625  seqf1oglem2a  10627  seqf1oglem2  10629  seq3id3  10633  seq3id  10634  seq3id2  10635  seq3homo  10636  seq3z  10637  seqfeq3  10638  seqhomog  10639  seqfeq4g  10640  ser3ge0  10645  expp1  10655  expnegap0  10656  expcllem  10659  mulexp  10687  expadd  10690  expaddzap  10692  expmulzap  10694  expdivap  10699  leexp1a  10703  expnlbnd  10773  bcpasc  10875  bccl  10876  hashfacen  10945  seq3coll  10951  seq3shft  11020  resqrexlemfp1  11191  sqrtdiv  11224  climshftlemg  11484  climcn1  11490  climsqz  11517  climsqz2  11518  clim2ser  11519  clim2ser2  11520  isermulc2  11522  climub  11526  serf0  11534  fsum3cvg  11560  sumrbdc  11561  summodclem3  11562  summodclem2a  11563  zsumdc  11566  fsumf1o  11572  isumss  11573  fisumss  11574  isumss2  11575  fsum3cvg2  11576  fsum3cvg3  11578  fsumcl2lem  11580  fsumcllem  11581  fsumadd  11588  fsumsplit  11589  fsumsplitsn  11592  sumsplitdc  11614  fisumrev2  11628  fsum2mul  11635  fsum00  11644  telfsumo  11648  fsumparts  11652  iserabs  11657  cvgratnnlemabsle  11709  cvgratnn  11713  cvgratz  11714  mertenslemub  11716  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  clim2prod  11721  clim2divap  11722  prodfap0  11727  prodfrecap  11728  prodeq2  11739  fproddccvg  11754  prodrbdclem2  11755  prodmodc  11760  zproddc  11761  fprodf1o  11770  fprodssdc  11772  fprodunsn  11786  fprodcllem  11788  fprodabs  11798  fprodeq0  11799  fprodmodd  11823  eftlcvg  11869  negdvdsb  11989  dvdsnegb  11990  fsumdvds  12024  dvdsext  12037  addmodlteqALT  12041  nno  12088  gcdsupex  12149  gcdsupcl  12150  bezoutlembz  12196  dvdssq  12223  eucalgf  12248  dvdslcm  12262  lcmledvds  12263  lcmeq0  12264  lcmcl  12265  lcmdvds  12272  lcmgcdeq  12276  divgcdcoprmex  12295  isprm5lem  12334  phibndlem  12409  phiprmpw  12415  pc2dvds  12524  pcmpt  12537  prmpwdvds  12549  1arith  12561  4sqleminfi  12591  ctiunctlemf  12680  ctiunct  12682  grpinva  13088  grprida  13089  gsumpropd2  13095  sgrppropd  13115  prdssgrpd  13117  mndpropd  13142  prdsidlem  13149  prdsmndd  13150  mhmpropd  13168  0mhm  13188  resmhm2  13190  resmhm2b  13191  grplcan  13264  mulgval  13328  mulgnn0z  13355  mulgnndir  13357  mulgnn0dir  13358  issubg2m  13395  issubg4m  13399  subgintm  13404  ghmf1  13479  gsumfzmptfidmadd  13545  gsumfzmhm  13549  srglmhm  13625  srgrmhm  13626  ringpropd  13670  crngpropd  13671  ringlghm  13693  ringrghm  13694  mulgass3  13717  issubrng2  13842  subrngpropd  13848  issubrg2  13873  subrgintm  13875  subrgpropd  13885  rhmpropd  13886  unitrrg  13899  lmodprop2d  13980  islss3  14011  lssintclm  14016  qusrhm  14160  gsumfzfsum  14220  opnssneib  14476  neissex  14485  tgrest  14489  iscnp3  14523  cnpnei  14539  cnrest  14555  tx1cn  14589  txcnp  14591  elbl3ps  14714  elbl3  14715  blininf  14744  blssexps  14749  blssex  14750  blpnfctr  14759  mopni2  14803  blsscls2  14813  metss  14814  bdmet  14822  metrest  14826  metcn  14834  txmetcn  14839  bl2ioo  14870  ivthinclemlr  14957  ivthinclemur  14959  dvcj  15029  dvfre  15030  elplyd  15061  plyaddlem1  15067  plymullem1  15068  plymullem  15070  plycolemc  15078  plycjlemc  15080  coseq0q4123  15154  abssinper  15166  fsumdvdsmul  15311  lgsval2lem  15335  lgsval4lem  15336  lgsneg  15349  lgsmod  15351  lgsdir2  15358  lgsdir  15360  lgsne0  15363  lgssq  15365  lgsquadlem1  15402  subctctexmid  15731  cvgcmp2n  15764  iswomninnlem  15780  nconstwlpo  15797