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  3888  pofun  4327  ralxfrd  4477  rexxfrd  4478  ordtri2or2exmidlem  4540  wessep  4592  poinxp  4710  relop  4792  fun11iun  5497  ssimaex  5593  fndmdif  5637  fconst2g  5747  foeqcnvco  5807  f1eqcocnv  5808  isocnv  5828  isocnv2  5829  riota2df  5867  f1o2ndf1  6247  tfr1onlembacc  6361  tfr1onlemaccex  6367  tfr1onlemres  6368  tfrcllembacc  6374  tfrcllemaccex  6380  tfrcllemres  6381  tfrcldm  6382  tfrcl  6383  xpdom2  6849  fimax2gtrilemstep  6918  xpfi  6947  eqsupti  7013  ordiso2  7052  enumctlemm  7131  enwomnilem  7185  cc2lem  7283  mulcanpig  7352  prarloclemlt  7510  genpdf  7525  genpdisj  7540  addnqprl  7546  addnqpru  7547  addlocpr  7553  prmuloc  7583  mulnqprl  7585  mulnqpru  7586  mullocpr  7588  ltpopr  7612  ltsopr  7613  ltaddpr  7614  ltexprlemdisj  7623  ltexprlemloc  7624  ltexprlemru  7629  addcanprleml  7631  addcanprlemu  7632  ltaprg  7636  recexprlemopu  7644  recexprlemloc  7648  cauappcvgprlemladdfl  7672  cauappcvgprlemladdru  7673  caucvgsrlemcau  7810  caucvgsrlemgt1  7812  caucvgsrlemoffcau  7815  caucvgsrlemoffres  7817  suplocsrlem  7825  axcaucvglemcau  7915  axpre-suploclemres  7918  axsuploc  8048  cnegexlem1  8150  cnegexlem3  8152  cnegex  8153  addsubeq4  8190  rimul  8560  divcanap6  8694  ltmul12a  8835  lemul12b  8836  lbinf  8923  zrevaddcl  9321  nzadd  9323  zextle  9362  fzind  9386  uz11  9568  infregelbex  9616  qreccl  9660  qrevaddcl  9662  irradd  9664  xrlttr  9813  xrltso  9814  xaddass  9887  xleadd1a  9891  xlt2add  9898  iccshftr  10012  iccshftl  10014  iccdil  10016  icccntr  10018  divelunit  10020  uzsubsubfz  10065  fzaddel  10077  fzrev  10102  elfzmlbp  10150  frec2uzrdg  10427  frecuzrdgtcl  10430  frecuzrdgsuc  10432  frecuzrdgdomlem  10435  frecuzrdgfunlem  10437  frecuzrdgsuctlem  10441  iseqovex  10474  seq3val  10476  seqf  10479  seq3clss  10485  seq3fveq2  10487  seq3feq2  10488  seq3feq  10490  seq3shft2  10491  ser3mono  10496  seq3split  10497  seq3caopr3  10499  seq3caopr2  10500  iseqf1olemab  10507  seq3f1olemqsumkj  10516  seq3f1olemqsumk  10517  seq3f1olemqsum  10518  seq3f1olemstep  10519  seq3f1oleml  10521  seq3id3  10525  seq3id  10526  seq3id2  10527  seq3homo  10528  seq3z  10529  seqfeq3  10530  ser3ge0  10535  expp1  10545  expnegap0  10546  expcllem  10549  mulexp  10577  expadd  10580  expaddzap  10582  expmulzap  10584  expdivap  10589  leexp1a  10593  expnlbnd  10663  bcpasc  10764  bccl  10765  hashfacen  10834  seq3coll  10840  seq3shft  10865  resqrexlemfp1  11036  sqrtdiv  11069  climshftlemg  11328  climcn1  11334  climsqz  11361  climsqz2  11362  clim2ser  11363  clim2ser2  11364  isermulc2  11366  climub  11370  serf0  11378  fsum3cvg  11404  sumrbdc  11405  summodclem3  11406  summodclem2a  11407  zsumdc  11410  fsumf1o  11416  isumss  11417  fisumss  11418  isumss2  11419  fsum3cvg2  11420  fsum3cvg3  11422  fsumcl2lem  11424  fsumcllem  11425  fsumadd  11432  fsumsplit  11433  fsumsplitsn  11436  sumsplitdc  11458  fisumrev2  11472  fsum2mul  11479  fsum00  11488  telfsumo  11492  fsumparts  11496  iserabs  11501  cvgratnnlemabsle  11553  cvgratnn  11557  cvgratz  11558  mertenslemub  11560  mertenslemi1  11561  mertenslem2  11562  mertensabs  11563  clim2prod  11565  clim2divap  11566  prodfap0  11571  prodfrecap  11572  prodeq2  11583  fproddccvg  11598  prodrbdclem2  11599  prodmodc  11604  zproddc  11605  fprodf1o  11614  fprodssdc  11616  fprodunsn  11630  fprodcllem  11632  fprodabs  11642  fprodeq0  11643  fprodmodd  11667  eftlcvg  11713  negdvdsb  11832  dvdsnegb  11833  dvdsext  11879  addmodlteqALT  11883  nno  11929  infssuzex  11968  zsupssdc  11973  gcdsupex  11976  gcdsupcl  11977  bezoutlembz  12023  dvdssq  12050  eucalgf  12073  dvdslcm  12087  lcmledvds  12088  lcmeq0  12089  lcmcl  12090  lcmdvds  12097  lcmgcdeq  12101  divgcdcoprmex  12120  isprm5lem  12159  phibndlem  12234  phiprmpw  12240  pc2dvds  12347  pcmpt  12359  prmpwdvds  12371  1arith  12383  ctiunctlemf  12457  ctiunct  12459  grpinva  12828  grprida  12829  sgrppropd  12842  mndpropd  12867  mhmpropd  12884  0mhm  12904  resmhm2  12906  resmhm2b  12907  grplcan  12972  mulgval  13030  mulgnn0z  13055  mulgnndir  13057  mulgnn0dir  13058  issubg2m  13094  issubg4m  13098  subgintm  13103  ghmf1  13173  srglmhm  13308  srgrmhm  13309  ringpropd  13353  crngpropd  13354  mulgass3  13396  issubrng2  13518  subrngpropd  13524  issubrg2  13549  subrgintm  13551  subrgpropd  13556  lmodprop2d  13625  islss3  13656  lssintclm  13661  opnssneib  14040  neissex  14049  tgrest  14053  iscnp3  14087  cnpnei  14103  cnrest  14119  tx1cn  14153  txcnp  14155  elbl3ps  14278  elbl3  14279  blininf  14308  blssexps  14313  blssex  14314  blpnfctr  14323  mopni2  14367  blsscls2  14377  metss  14378  bdmet  14386  metrest  14390  metcn  14398  txmetcn  14403  bl2ioo  14426  ivthinclemlr  14499  ivthinclemur  14501  dvcj  14557  dvfre  14558  coseq0q4123  14639  abssinper  14651  lgsval2lem  14795  lgsval4lem  14796  lgsneg  14809  lgsmod  14811  lgsdir2  14818  lgsdir  14820  lgsne0  14823  lgssq  14825  subctctexmid  15135  cvgcmp2n  15166  iswomninnlem  15182  nconstwlpo  15199