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  3903  pofun  4347  ralxfrd  4497  rexxfrd  4498  ordtri2or2exmidlem  4562  wessep  4614  poinxp  4732  relop  4816  fun11iun  5525  ssimaex  5622  fndmdif  5667  fconst2g  5777  foeqcnvco  5837  f1eqcocnv  5838  isocnv  5858  isocnv2  5859  riota2df  5898  caofdig  6164  f1o2ndf1  6286  tfr1onlembacc  6400  tfr1onlemaccex  6406  tfr1onlemres  6407  tfrcllembacc  6413  tfrcllemaccex  6419  tfrcllemres  6420  tfrcldm  6421  tfrcl  6422  xpdom2  6890  fimax2gtrilemstep  6961  xpfi  6993  eqsupti  7062  ordiso2  7101  enumctlemm  7180  enwomnilem  7235  cc2lem  7333  mulcanpig  7402  prarloclemlt  7560  genpdf  7575  genpdisj  7590  addnqprl  7596  addnqpru  7597  addlocpr  7603  prmuloc  7633  mulnqprl  7635  mulnqpru  7636  mullocpr  7638  ltpopr  7662  ltsopr  7663  ltaddpr  7664  ltexprlemdisj  7673  ltexprlemloc  7674  ltexprlemru  7679  addcanprleml  7681  addcanprlemu  7682  ltaprg  7686  recexprlemopu  7694  recexprlemloc  7698  cauappcvgprlemladdfl  7722  cauappcvgprlemladdru  7723  caucvgsrlemcau  7860  caucvgsrlemgt1  7862  caucvgsrlemoffcau  7865  caucvgsrlemoffres  7867  suplocsrlem  7875  axcaucvglemcau  7965  axpre-suploclemres  7968  axsuploc  8099  cnegexlem1  8201  cnegexlem3  8203  cnegex  8204  addsubeq4  8241  rimul  8612  divcanap6  8746  ltmul12a  8887  lemul12b  8888  lbinf  8975  zrevaddcl  9376  nzadd  9378  zextle  9417  fzind  9441  uz11  9624  infregelbex  9672  qreccl  9716  qrevaddcl  9718  irradd  9720  xrlttr  9870  xrltso  9871  xaddass  9944  xleadd1a  9948  xlt2add  9955  iccshftr  10069  iccshftl  10071  iccdil  10073  icccntr  10075  divelunit  10077  uzsubsubfz  10122  fzaddel  10134  fzrev  10159  elfzmlbp  10207  infssuzex  10323  zsupssdc  10328  frec2uzrdg  10501  frecuzrdgtcl  10504  frecuzrdgsuc  10506  frecuzrdgdomlem  10509  frecuzrdgfunlem  10511  frecuzrdgsuctlem  10515  iseqovex  10550  seq3val  10552  seqf  10556  seq3clss  10563  seq3fveq2  10567  seq3feq2  10568  seq3feq  10572  seq3shft2  10573  ser3mono  10579  seq3split  10580  seqsplitg  10581  seq3caopr3  10583  seq3caopr2  10585  seqcaopr2g  10586  iseqf1olemab  10594  seq3f1olemqsumkj  10603  seq3f1olemqsumk  10604  seq3f1olemqsum  10605  seq3f1olemstep  10606  seq3f1oleml  10608  seqf1oglem2a  10610  seqf1oglem2  10612  seq3id3  10616  seq3id  10617  seq3id2  10618  seq3homo  10619  seq3z  10620  seqfeq3  10621  seqhomog  10622  seqfeq4g  10623  ser3ge0  10628  expp1  10638  expnegap0  10639  expcllem  10642  mulexp  10670  expadd  10673  expaddzap  10675  expmulzap  10677  expdivap  10682  leexp1a  10686  expnlbnd  10756  bcpasc  10858  bccl  10859  hashfacen  10928  seq3coll  10934  seq3shft  11003  resqrexlemfp1  11174  sqrtdiv  11207  climshftlemg  11467  climcn1  11473  climsqz  11500  climsqz2  11501  clim2ser  11502  clim2ser2  11503  isermulc2  11505  climub  11509  serf0  11517  fsum3cvg  11543  sumrbdc  11544  summodclem3  11545  summodclem2a  11546  zsumdc  11549  fsumf1o  11555  isumss  11556  fisumss  11557  isumss2  11558  fsum3cvg2  11559  fsum3cvg3  11561  fsumcl2lem  11563  fsumcllem  11564  fsumadd  11571  fsumsplit  11572  fsumsplitsn  11575  sumsplitdc  11597  fisumrev2  11611  fsum2mul  11618  fsum00  11627  telfsumo  11631  fsumparts  11635  iserabs  11640  cvgratnnlemabsle  11692  cvgratnn  11696  cvgratz  11697  mertenslemub  11699  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  clim2prod  11704  clim2divap  11705  prodfap0  11710  prodfrecap  11711  prodeq2  11722  fproddccvg  11737  prodrbdclem2  11738  prodmodc  11743  zproddc  11744  fprodf1o  11753  fprodssdc  11755  fprodunsn  11769  fprodcllem  11771  fprodabs  11781  fprodeq0  11782  fprodmodd  11806  eftlcvg  11852  negdvdsb  11972  dvdsnegb  11973  fsumdvds  12007  dvdsext  12020  addmodlteqALT  12024  nno  12071  gcdsupex  12124  gcdsupcl  12125  bezoutlembz  12171  dvdssq  12198  eucalgf  12223  dvdslcm  12237  lcmledvds  12238  lcmeq0  12239  lcmcl  12240  lcmdvds  12247  lcmgcdeq  12251  divgcdcoprmex  12270  isprm5lem  12309  phibndlem  12384  phiprmpw  12390  pc2dvds  12499  pcmpt  12512  prmpwdvds  12524  1arith  12536  4sqleminfi  12566  ctiunctlemf  12655  ctiunct  12657  grpinva  13029  grprida  13030  gsumpropd2  13036  sgrppropd  13056  mndpropd  13081  mhmpropd  13098  0mhm  13118  resmhm2  13120  resmhm2b  13121  grplcan  13194  mulgval  13252  mulgnn0z  13279  mulgnndir  13281  mulgnn0dir  13282  issubg2m  13319  issubg4m  13323  subgintm  13328  ghmf1  13403  gsumfzmptfidmadd  13469  gsumfzmhm  13473  srglmhm  13549  srgrmhm  13550  ringpropd  13594  crngpropd  13595  ringlghm  13617  ringrghm  13618  mulgass3  13641  issubrng2  13766  subrngpropd  13772  issubrg2  13797  subrgintm  13799  subrgpropd  13809  rhmpropd  13810  unitrrg  13823  lmodprop2d  13904  islss3  13935  lssintclm  13940  qusrhm  14084  gsumfzfsum  14144  opnssneib  14392  neissex  14401  tgrest  14405  iscnp3  14439  cnpnei  14455  cnrest  14471  tx1cn  14505  txcnp  14507  elbl3ps  14630  elbl3  14631  blininf  14660  blssexps  14665  blssex  14666  blpnfctr  14675  mopni2  14719  blsscls2  14729  metss  14730  bdmet  14738  metrest  14742  metcn  14750  txmetcn  14755  bl2ioo  14786  ivthinclemlr  14873  ivthinclemur  14875  dvcj  14945  dvfre  14946  elplyd  14977  plyaddlem1  14983  plymullem1  14984  plymullem  14986  plycolemc  14994  plycjlemc  14996  coseq0q4123  15070  abssinper  15082  fsumdvdsmul  15227  lgsval2lem  15251  lgsval4lem  15252  lgsneg  15265  lgsmod  15267  lgsdir2  15274  lgsdir  15276  lgsne0  15279  lgssq  15281  lgsquadlem1  15318  subctctexmid  15645  cvgcmp2n  15677  iswomninnlem  15693  nconstwlpo  15710