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  1162  3ad2antl2  1163  ad4ant124  1219  3adant1r  1234  ad5ant235  1241  ad5ant135  1246  bilukdc  1416  intab  3919  pofun  4366  ralxfrd  4516  rexxfrd  4517  ordtri2or2exmidlem  4581  wessep  4633  poinxp  4751  relop  4835  fun11iun  5554  ssimaex  5652  fndmdif  5697  fconst2g  5811  foeqcnvco  5871  f1eqcocnv  5872  isocnv  5892  isocnv2  5893  riota2df  5932  caofdig  6204  f1o2ndf1  6326  tfr1onlembacc  6440  tfr1onlemaccex  6446  tfr1onlemres  6447  tfrcllembacc  6453  tfrcllemaccex  6459  tfrcllemres  6460  tfrcldm  6461  tfrcl  6462  xpdom2  6940  fimax2gtrilemstep  7011  xpfi  7043  eqsupti  7112  ordiso2  7151  enumctlemm  7230  enwomnilem  7285  cc2lem  7393  mulcanpig  7463  prarloclemlt  7621  genpdf  7636  genpdisj  7651  addnqprl  7657  addnqpru  7658  addlocpr  7664  prmuloc  7694  mulnqprl  7696  mulnqpru  7697  mullocpr  7699  ltpopr  7723  ltsopr  7724  ltaddpr  7725  ltexprlemdisj  7734  ltexprlemloc  7735  ltexprlemru  7740  addcanprleml  7742  addcanprlemu  7743  ltaprg  7747  recexprlemopu  7755  recexprlemloc  7759  cauappcvgprlemladdfl  7783  cauappcvgprlemladdru  7784  caucvgsrlemcau  7921  caucvgsrlemgt1  7923  caucvgsrlemoffcau  7926  caucvgsrlemoffres  7928  suplocsrlem  7936  axcaucvglemcau  8026  axpre-suploclemres  8029  axsuploc  8160  cnegexlem1  8262  cnegexlem3  8264  cnegex  8265  addsubeq4  8302  rimul  8673  divcanap6  8807  ltmul12a  8948  lemul12b  8949  lbinf  9036  zrevaddcl  9438  nzadd  9440  zextle  9479  fzind  9503  uz11  9686  infregelbex  9734  qreccl  9778  qrevaddcl  9780  irradd  9782  xrlttr  9932  xrltso  9933  xaddass  10006  xleadd1a  10010  xlt2add  10017  iccshftr  10131  iccshftl  10133  iccdil  10135  icccntr  10137  divelunit  10139  uzsubsubfz  10184  fzaddel  10196  fzrev  10221  elfzmlbp  10269  infssuzex  10393  zsupssdc  10398  frec2uzrdg  10571  frecuzrdgtcl  10574  frecuzrdgsuc  10576  frecuzrdgdomlem  10579  frecuzrdgfunlem  10581  frecuzrdgsuctlem  10585  iseqovex  10620  seq3val  10622  seqf  10626  seq3clss  10633  seq3fveq2  10637  seq3feq2  10638  seq3feq  10642  seq3shft2  10643  ser3mono  10649  seq3split  10650  seqsplitg  10651  seq3caopr3  10653  seq3caopr2  10655  seqcaopr2g  10656  iseqf1olemab  10664  seq3f1olemqsumkj  10673  seq3f1olemqsumk  10674  seq3f1olemqsum  10675  seq3f1olemstep  10676  seq3f1oleml  10678  seqf1oglem2a  10680  seqf1oglem2  10682  seq3id3  10686  seq3id  10687  seq3id2  10688  seq3homo  10689  seq3z  10690  seqfeq3  10691  seqhomog  10692  seqfeq4g  10693  ser3ge0  10698  expp1  10708  expnegap0  10709  expcllem  10712  mulexp  10740  expadd  10743  expaddzap  10745  expmulzap  10747  expdivap  10752  leexp1a  10756  expnlbnd  10826  bcpasc  10928  bccl  10929  hashfacen  10998  seq3coll  11004  ccatlen  11069  ccatvalfn  11075  ccatsymb  11076  pfxclz  11150  wrd2ind  11194  seq3shft  11219  resqrexlemfp1  11390  sqrtdiv  11423  climshftlemg  11683  climcn1  11689  climsqz  11716  climsqz2  11717  clim2ser  11718  clim2ser2  11719  isermulc2  11721  climub  11725  serf0  11733  fsum3cvg  11759  sumrbdc  11760  summodclem3  11761  summodclem2a  11762  zsumdc  11765  fsumf1o  11771  isumss  11772  fisumss  11773  isumss2  11774  fsum3cvg2  11775  fsum3cvg3  11777  fsumcl2lem  11779  fsumcllem  11780  fsumadd  11787  fsumsplit  11788  fsumsplitsn  11791  sumsplitdc  11813  fisumrev2  11827  fsum2mul  11834  fsum00  11843  telfsumo  11847  fsumparts  11851  iserabs  11856  cvgratnnlemabsle  11908  cvgratnn  11912  cvgratz  11913  mertenslemub  11915  mertenslemi1  11916  mertenslem2  11917  mertensabs  11918  clim2prod  11920  clim2divap  11921  prodfap0  11926  prodfrecap  11927  prodeq2  11938  fproddccvg  11953  prodrbdclem2  11954  prodmodc  11959  zproddc  11960  fprodf1o  11969  fprodssdc  11971  fprodunsn  11985  fprodcllem  11987  fprodabs  11997  fprodeq0  11998  fprodmodd  12022  eftlcvg  12068  negdvdsb  12188  dvdsnegb  12189  fsumdvds  12223  dvdsext  12236  addmodlteqALT  12240  nno  12287  gcdsupex  12348  gcdsupcl  12349  bezoutlembz  12395  dvdssq  12422  eucalgf  12447  dvdslcm  12461  lcmledvds  12462  lcmeq0  12463  lcmcl  12464  lcmdvds  12471  lcmgcdeq  12475  divgcdcoprmex  12494  isprm5lem  12533  phibndlem  12608  phiprmpw  12614  pc2dvds  12723  pcmpt  12736  prmpwdvds  12748  1arith  12760  4sqleminfi  12790  ctiunctlemf  12879  ctiunct  12881  grpinva  13288  grprida  13289  gsumpropd2  13295  sgrppropd  13315  prdssgrpd  13317  mndpropd  13342  prdsidlem  13349  prdsmndd  13350  mhmpropd  13368  0mhm  13388  resmhm2  13390  resmhm2b  13391  grplcan  13464  mulgval  13528  mulgnn0z  13555  mulgnndir  13557  mulgnn0dir  13558  issubg2m  13595  issubg4m  13599  subgintm  13604  ghmf1  13679  gsumfzmptfidmadd  13745  gsumfzmhm  13749  srglmhm  13825  srgrmhm  13826  ringpropd  13870  crngpropd  13871  ringlghm  13893  ringrghm  13894  mulgass3  13917  issubrng2  14042  subrngpropd  14048  issubrg2  14073  subrgintm  14075  subrgpropd  14085  rhmpropd  14086  unitrrg  14099  lmodprop2d  14180  islss3  14211  lssintclm  14216  qusrhm  14360  gsumfzfsum  14420  opnssneib  14698  neissex  14707  tgrest  14711  iscnp3  14745  cnpnei  14761  cnrest  14777  tx1cn  14811  txcnp  14813  elbl3ps  14936  elbl3  14937  blininf  14966  blssexps  14971  blssex  14972  blpnfctr  14981  mopni2  15025  blsscls2  15035  metss  15036  bdmet  15044  metrest  15048  metcn  15056  txmetcn  15061  bl2ioo  15092  ivthinclemlr  15179  ivthinclemur  15181  dvcj  15251  dvfre  15252  elplyd  15283  plyaddlem1  15289  plymullem1  15290  plymullem  15292  plycolemc  15300  plycjlemc  15302  coseq0q4123  15376  abssinper  15388  fsumdvdsmul  15533  lgsval2lem  15557  lgsval4lem  15558  lgsneg  15571  lgsmod  15573  lgsdir2  15580  lgsdir  15582  lgsne0  15585  lgssq  15587  lgsquadlem1  15624  subctctexmid  16072  cvgcmp2n  16107  iswomninnlem  16123  nconstwlpo  16140