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  3864  intab  3962  pofun  4415  ralxfrd  4565  rexxfrd  4566  ordtri2or2exmidlem  4630  wessep  4682  poinxp  4801  relop  4886  fun11iun  5613  ssimaex  5716  fndmdif  5761  fconst2g  5877  foeqcnvco  5941  f1eqcocnv  5942  isocnv  5962  isocnv2  5963  riota2df  6003  caofdig  6278  f1o2ndf1  6402  tfr1onlembacc  6551  tfr1onlemaccex  6557  tfr1onlemres  6558  tfrcllembacc  6564  tfrcllemaccex  6570  tfrcllemres  6571  tfrcldm  6572  tfrcl  6573  xpdom2  7058  fimax2gtrilemstep  7133  xpfi  7167  eqsupti  7238  ordiso2  7277  enumctlemm  7356  enwomnilem  7411  cc2lem  7528  mulcanpig  7598  prarloclemlt  7756  genpdf  7771  genpdisj  7786  addnqprl  7792  addnqpru  7793  addlocpr  7799  prmuloc  7829  mulnqprl  7831  mulnqpru  7832  mullocpr  7834  ltpopr  7858  ltsopr  7859  ltaddpr  7860  ltexprlemdisj  7869  ltexprlemloc  7870  ltexprlemru  7875  addcanprleml  7877  addcanprlemu  7878  ltaprg  7882  recexprlemopu  7890  recexprlemloc  7894  cauappcvgprlemladdfl  7918  cauappcvgprlemladdru  7919  caucvgsrlemcau  8056  caucvgsrlemgt1  8058  caucvgsrlemoffcau  8061  caucvgsrlemoffres  8063  suplocsrlem  8071  axcaucvglemcau  8161  axpre-suploclemres  8164  axsuploc  8295  cnegexlem1  8397  cnegexlem3  8399  cnegex  8400  addsubeq4  8437  rimul  8808  divcanap6  8942  ltmul12a  9083  lemul12b  9084  lbinf  9171  zrevaddcl  9573  nzadd  9575  zextle  9614  fzind  9638  uz11  9822  infregelbex  9875  qreccl  9919  qrevaddcl  9921  irradd  9923  xrlttr  10073  xrltso  10074  xaddass  10147  xleadd1a  10151  xlt2add  10158  iccshftr  10272  iccshftl  10274  iccdil  10276  icccntr  10278  divelunit  10280  uzsubsubfz  10325  fzaddel  10337  fzrev  10362  elfzmlbp  10410  infssuzex  10537  zsupssdc  10542  frec2uzrdg  10715  frecuzrdgtcl  10718  frecuzrdgsuc  10720  frecuzrdgdomlem  10723  frecuzrdgfunlem  10725  frecuzrdgsuctlem  10729  iseqovex  10764  seq3val  10766  seqf  10770  seq3clss  10777  seq3fveq2  10781  seq3feq2  10782  seq3feq  10786  seq3shft2  10787  ser3mono  10793  seq3split  10794  seqsplitg  10795  seq3caopr3  10797  seq3caopr2  10799  seqcaopr2g  10800  iseqf1olemab  10808  seq3f1olemqsumkj  10817  seq3f1olemqsumk  10818  seq3f1olemqsum  10819  seq3f1olemstep  10820  seq3f1oleml  10822  seqf1oglem2a  10824  seqf1oglem2  10826  seq3id3  10830  seq3id  10831  seq3id2  10832  seq3homo  10833  seq3z  10834  seqfeq3  10835  seqhomog  10836  seqfeq4g  10837  ser3ge0  10842  expp1  10852  expnegap0  10853  expcllem  10856  mulexp  10884  expadd  10887  expaddzap  10889  expmulzap  10891  expdivap  10896  leexp1a  10900  expnlbnd  10970  bcpasc  11072  bccl  11073  hashfacen  11144  seq3coll  11150  ccatlen  11219  ccatvalfn  11225  ccatsymb  11226  ccatalpha  11237  pfxclz  11307  wrd2ind  11351  swrdccat  11363  seq3shft  11459  resqrexlemfp1  11630  sqrtdiv  11663  climshftlemg  11923  climcn1  11929  climsqz  11956  climsqz2  11957  clim2ser  11958  clim2ser2  11959  isermulc2  11961  climub  11965  serf0  11973  fsum3cvg  12000  sumrbdc  12001  summodclem3  12002  summodclem2a  12003  zsumdc  12006  fsumf1o  12012  isumss  12013  fisumss  12014  isumss2  12015  fsum3cvg2  12016  fsum3cvg3  12018  fsumcl2lem  12020  fsumcllem  12021  fsumadd  12028  fsumsplit  12029  fsumsplitsn  12032  sumsplitdc  12054  fisumrev2  12068  fsum2mul  12075  fsum00  12084  telfsumo  12088  fsumparts  12092  iserabs  12097  cvgratnnlemabsle  12149  cvgratnn  12153  cvgratz  12154  mertenslemub  12156  mertenslemi1  12157  mertenslem2  12158  mertensabs  12159  clim2prod  12161  clim2divap  12162  prodfap0  12167  prodfrecap  12168  prodeq2  12179  fproddccvg  12194  prodrbdclem2  12195  prodmodc  12200  zproddc  12201  fprodf1o  12210  fprodssdc  12212  fprodunsn  12226  fprodcllem  12228  fprodabs  12238  fprodeq0  12239  fprodmodd  12263  eftlcvg  12309  negdvdsb  12429  dvdsnegb  12430  fsumdvds  12464  dvdsext  12477  addmodlteqALT  12481  nno  12528  gcdsupex  12589  gcdsupcl  12590  bezoutlembz  12636  dvdssq  12663  eucalgf  12688  dvdslcm  12702  lcmledvds  12703  lcmeq0  12704  lcmcl  12705  lcmdvds  12712  lcmgcdeq  12716  divgcdcoprmex  12735  isprm5lem  12774  phibndlem  12849  phiprmpw  12855  pc2dvds  12964  pcmpt  12977  prmpwdvds  12989  1arith  13001  4sqleminfi  13031  ctiunctlemf  13120  ctiunct  13122  grpinva  13530  grprida  13531  gsumpropd2  13537  sgrppropd  13557  prdssgrpd  13559  mndpropd  13584  prdsidlem  13591  prdsmndd  13592  mhmpropd  13610  0mhm  13630  resmhm2  13632  resmhm2b  13633  grplcan  13706  mulgval  13770  mulgnn0z  13797  mulgnndir  13799  mulgnn0dir  13800  issubg2m  13837  issubg4m  13841  subgintm  13846  ghmf1  13921  gsumfzmptfidmadd  13987  gsumfzmhm  13991  srglmhm  14068  srgrmhm  14069  ringpropd  14113  crngpropd  14114  ringlghm  14136  ringrghm  14137  mulgass3  14160  issubrng2  14286  subrngpropd  14292  issubrg2  14317  subrgintm  14319  subrgpropd  14329  rhmpropd  14330  unitrrg  14343  lmodprop2d  14424  islss3  14455  lssintclm  14460  qusrhm  14604  gsumfzfsum  14664  opnssneib  14947  neissex  14956  tgrest  14960  iscnp3  14994  cnpnei  15010  cnrest  15026  tx1cn  15060  txcnp  15062  elbl3ps  15185  elbl3  15186  blininf  15215  blssexps  15220  blssex  15221  blpnfctr  15230  mopni2  15274  blsscls2  15284  metss  15285  bdmet  15293  metrest  15297  metcn  15305  txmetcn  15310  bl2ioo  15341  ivthinclemlr  15428  ivthinclemur  15430  dvcj  15500  dvfre  15501  elplyd  15532  plyaddlem1  15538  plymullem1  15539  plymullem  15541  plycolemc  15549  plycjlemc  15551  coseq0q4123  15625  abssinper  15637  fsumdvdsmul  15785  lgsval2lem  15809  lgsval4lem  15810  lgsneg  15823  lgsmod  15825  lgsdir2  15832  lgsdir  15834  lgsne0  15837  lgssq  15839  lgsquadlem1  15876  usgredg2vlem2  16144  clwwlkccat  16322  clwwlknonex2lem2  16359  subctctexmid  16702  cvgcmp2n  16745  iswomninnlem  16762  nconstwlpo  16779