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  3899  pofun  4343  ralxfrd  4493  rexxfrd  4494  ordtri2or2exmidlem  4558  wessep  4610  poinxp  4728  relop  4812  fun11iun  5521  ssimaex  5618  fndmdif  5663  fconst2g  5773  foeqcnvco  5833  f1eqcocnv  5834  isocnv  5854  isocnv2  5855  riota2df  5894  caofdig  6159  f1o2ndf1  6281  tfr1onlembacc  6395  tfr1onlemaccex  6401  tfr1onlemres  6402  tfrcllembacc  6408  tfrcllemaccex  6414  tfrcllemres  6415  tfrcldm  6416  tfrcl  6417  xpdom2  6885  fimax2gtrilemstep  6956  xpfi  6986  eqsupti  7055  ordiso2  7094  enumctlemm  7173  enwomnilem  7228  cc2lem  7326  mulcanpig  7395  prarloclemlt  7553  genpdf  7568  genpdisj  7583  addnqprl  7589  addnqpru  7590  addlocpr  7596  prmuloc  7626  mulnqprl  7628  mulnqpru  7629  mullocpr  7631  ltpopr  7655  ltsopr  7656  ltaddpr  7657  ltexprlemdisj  7666  ltexprlemloc  7667  ltexprlemru  7672  addcanprleml  7674  addcanprlemu  7675  ltaprg  7679  recexprlemopu  7687  recexprlemloc  7691  cauappcvgprlemladdfl  7715  cauappcvgprlemladdru  7716  caucvgsrlemcau  7853  caucvgsrlemgt1  7855  caucvgsrlemoffcau  7858  caucvgsrlemoffres  7860  suplocsrlem  7868  axcaucvglemcau  7958  axpre-suploclemres  7961  axsuploc  8092  cnegexlem1  8194  cnegexlem3  8196  cnegex  8197  addsubeq4  8234  rimul  8604  divcanap6  8738  ltmul12a  8879  lemul12b  8880  lbinf  8967  zrevaddcl  9367  nzadd  9369  zextle  9408  fzind  9432  uz11  9615  infregelbex  9663  qreccl  9707  qrevaddcl  9709  irradd  9711  xrlttr  9861  xrltso  9862  xaddass  9935  xleadd1a  9939  xlt2add  9946  iccshftr  10060  iccshftl  10062  iccdil  10064  icccntr  10066  divelunit  10068  uzsubsubfz  10113  fzaddel  10125  fzrev  10150  elfzmlbp  10198  frec2uzrdg  10480  frecuzrdgtcl  10483  frecuzrdgsuc  10485  frecuzrdgdomlem  10488  frecuzrdgfunlem  10490  frecuzrdgsuctlem  10494  iseqovex  10529  seq3val  10531  seqf  10535  seq3clss  10542  seq3fveq2  10546  seq3feq2  10547  seq3feq  10551  seq3shft2  10552  ser3mono  10558  seq3split  10559  seqsplitg  10560  seq3caopr3  10562  seq3caopr2  10564  seqcaopr2g  10565  iseqf1olemab  10573  seq3f1olemqsumkj  10582  seq3f1olemqsumk  10583  seq3f1olemqsum  10584  seq3f1olemstep  10585  seq3f1oleml  10587  seqf1oglem2a  10589  seqf1oglem2  10591  seq3id3  10595  seq3id  10596  seq3id2  10597  seq3homo  10598  seq3z  10599  seqfeq3  10600  seqhomog  10601  seqfeq4g  10602  ser3ge0  10607  expp1  10617  expnegap0  10618  expcllem  10621  mulexp  10649  expadd  10652  expaddzap  10654  expmulzap  10656  expdivap  10661  leexp1a  10665  expnlbnd  10735  bcpasc  10837  bccl  10838  hashfacen  10907  seq3coll  10913  seq3shft  10982  resqrexlemfp1  11153  sqrtdiv  11186  climshftlemg  11445  climcn1  11451  climsqz  11478  climsqz2  11479  clim2ser  11480  clim2ser2  11481  isermulc2  11483  climub  11487  serf0  11495  fsum3cvg  11521  sumrbdc  11522  summodclem3  11523  summodclem2a  11524  zsumdc  11527  fsumf1o  11533  isumss  11534  fisumss  11535  isumss2  11536  fsum3cvg2  11537  fsum3cvg3  11539  fsumcl2lem  11541  fsumcllem  11542  fsumadd  11549  fsumsplit  11550  fsumsplitsn  11553  sumsplitdc  11575  fisumrev2  11589  fsum2mul  11596  fsum00  11605  telfsumo  11609  fsumparts  11613  iserabs  11618  cvgratnnlemabsle  11670  cvgratnn  11674  cvgratz  11675  mertenslemub  11677  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  clim2prod  11682  clim2divap  11683  prodfap0  11688  prodfrecap  11689  prodeq2  11700  fproddccvg  11715  prodrbdclem2  11716  prodmodc  11721  zproddc  11722  fprodf1o  11731  fprodssdc  11733  fprodunsn  11747  fprodcllem  11749  fprodabs  11759  fprodeq0  11760  fprodmodd  11784  eftlcvg  11830  negdvdsb  11950  dvdsnegb  11951  dvdsext  11997  addmodlteqALT  12001  nno  12047  infssuzex  12086  zsupssdc  12091  gcdsupex  12094  gcdsupcl  12095  bezoutlembz  12141  dvdssq  12168  eucalgf  12193  dvdslcm  12207  lcmledvds  12208  lcmeq0  12209  lcmcl  12210  lcmdvds  12217  lcmgcdeq  12221  divgcdcoprmex  12240  isprm5lem  12279  phibndlem  12354  phiprmpw  12360  pc2dvds  12468  pcmpt  12481  prmpwdvds  12493  1arith  12505  4sqleminfi  12535  ctiunctlemf  12595  ctiunct  12597  grpinva  12969  grprida  12970  gsumpropd2  12976  sgrppropd  12996  mndpropd  13021  mhmpropd  13038  0mhm  13058  resmhm2  13060  resmhm2b  13061  grplcan  13134  mulgval  13192  mulgnn0z  13219  mulgnndir  13221  mulgnn0dir  13222  issubg2m  13259  issubg4m  13263  subgintm  13268  ghmf1  13343  gsumfzmptfidmadd  13409  gsumfzmhm  13413  srglmhm  13489  srgrmhm  13490  ringpropd  13534  crngpropd  13535  ringlghm  13557  ringrghm  13558  mulgass3  13581  issubrng2  13706  subrngpropd  13712  issubrg2  13737  subrgintm  13739  subrgpropd  13749  rhmpropd  13750  unitrrg  13763  lmodprop2d  13844  islss3  13875  lssintclm  13880  qusrhm  14024  gsumfzfsum  14076  opnssneib  14324  neissex  14333  tgrest  14337  iscnp3  14371  cnpnei  14387  cnrest  14403  tx1cn  14437  txcnp  14439  elbl3ps  14562  elbl3  14563  blininf  14592  blssexps  14597  blssex  14598  blpnfctr  14607  mopni2  14651  blsscls2  14661  metss  14662  bdmet  14670  metrest  14674  metcn  14682  txmetcn  14687  bl2ioo  14710  ivthinclemlr  14791  ivthinclemur  14793  dvcj  14858  dvfre  14859  elplyd  14887  plyaddlem1  14893  plymullem1  14894  plymullem  14896  coseq0q4123  14969  abssinper  14981  lgsval2lem  15126  lgsval4lem  15127  lgsneg  15140  lgsmod  15142  lgsdir2  15149  lgsdir  15151  lgsne0  15154  lgssq  15156  lgsquadlem1  15191  subctctexmid  15491  cvgcmp2n  15523  iswomninnlem  15539  nconstwlpo  15556