Theorem ad2antlr 489

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)

Hypothesis

Ref	Expression
ad2ant.1	|- ( ph -> ps )

Assertion

Ref	Expression
ad2antlr	|- ( ( ( ch /\ ph ) /\ th ) -> ps )

Proof of Theorem ad2antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	adantr 276	. 2 |- ( ( ph /\ th ) -> ps )
3	2	adantll 476	1 |- ( ( ( ch /\ ph ) /\ th ) -> ps )

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:  ad3antlr  493  simplr  528  simplrl  535  simplrr  536  ordtri2or2exmidlem  4618  en2lp  4646  foun  5593  f1oprg  5619  fcof1o  5919  foeqcnvco  5920  f1eqcocnv  5921  caovord3  6185  f1o2ndf1  6380  smores2  6446  frecrdg  6560  nnaordex  6682  xpdom2  6998  xpen  7014  mapen  7015  xpmapenlem  7018  nndomo  7033  phpm  7035  fidifsnen  7040  isinfinf  7067  fidcen  7069  finexdc  7073  elssdc  7075  fientri3  7088  fiintim  7104  xpfi  7105  f1dmvrnfibi  7122  sbthlemi8  7142  djudom  7271  omp1eomlem  7272  difinfsn  7278  ctmlemr  7286  ctssdccl  7289  nnnninfeq  7306  enomnilem  7316  finomni  7318  ismkvnex  7333  enmkvlem  7339  nninfwlpoimlemginf  7354  exmidfodomrlemrALT  7392  exmidontriim  7418  netap  7451  exmidapne  7457  acnccim  7469  dfplpq2  7552  recclnq  7590  subhalfnqq  7612  distrnq0  7657  prarloclem3step  7694  genpml  7715  genpmu  7716  addnqprl  7727  addnqpru  7728  appdivnq  7761  mulnqprl  7766  mulnqpru  7767  mullocpr  7769  ltexprlemfl  7807  ltexprlemfu  7809  ltmprr  7840  archpr  7841  cauappcvgprlemm  7843  caucvgprlemladdrl  7876  caucvgprprlemopl  7895  caucvgprprlemopu  7897  recexgt0sr  7971  mulgt0sr  7976  elrealeu  8027  axcaucvglemcau  8096  axcaucvglemres  8097  cnegex  8335  apirr  8763  mulge0  8777  lemul12a  9020  lediv2a  9053  creur  9117  nndiv  9162  zaddcllemneg  9496  peano5uzti  9566  supinfneg  9802  infsupneg  9803  divfnzn  9828  xrltso  10004  xpncan  10079  xltadd1  10084  xleaddadd  10095  elioc2  10144  elico2  10145  elicc2  10146  exfzdc  10458  zsupcllemstep  10461  infssuzex  10465  suprzubdc  10468  exbtwnzlemex  10481  rebtwn2z  10486  modqid  10583  modqcyc  10593  mulqaddmodid  10598  modqadd2mod  10608  addmodlteq  10632  frecuzrdgg  10650  nninfinf  10677  seq3val  10694  seqvalcd  10695  seq3clss  10705  iseqf1olemqcl  10733  iseqf1olemnab  10735  seq3f1olemp  10749  seq3f1o  10751  seqf1oglem1  10753  seqfeq4g  10765  fser0const  10769  ser3ge0  10770  exp3vallem  10774  qsqeqor  10884  facndiv  10973  faclbnd  10975  bcval5  10997  hashen  11018  fihashdom  11037  hashunlem  11038  hashfacen  11071  zfz1isolemiso  11074  seq3coll  11077  ccatsymb  11150  ccatrn  11157  ccatw2s1p2  11191  swrdccatin1  11272  swrdccatin2  11276  swrdccat3b  11287  caucvgre  11507  resqrexlemlo  11539  cau3lem  11640  qdenre  11728  rexico  11747  fimaxre2  11753  2zinfmin  11769  xrmaxiflemcl  11771  xrmaxifle  11772  xrmaxiflemcom  11775  2clim  11827  cn1lem  11840  climsqz  11861  climsqz2  11862  climcau  11873  sumrbdclem  11903  summodclem2a  11907  fsum3  11913  fsumcl2lem  11924  fsumadd  11932  sumsnf  11935  fsum2dlemstep  11960  fisum0diag2  11973  fsummulc2  11974  mertenslemub  12060  mertenslemi1  12061  mertensabs  12063  ntrivcvgap  12074  prodrbdclem  12097  prodmodclem3  12101  prodmodclem2a  12102  prodmodc  12104  prod1dc  12112  prodsnf  12118  fprod2dlemstep  12148  efaddlem  12200  tanaddaplem  12264  zdvdsdc  12338  dvdseq  12374  dvdsext  12381  odd2np1  12399  sqoddm1div8z  12412  nno  12432  dfgcd3  12546  nninfctlemfo  12576  dvdslcm  12606  lcmneg  12611  lcmgcdlem  12614  ncoprmgcdne1b  12626  qredeq  12633  qredeu  12634  divgcdcoprm0  12638  exprmfct  12675  prmdvdsfz  12676  isprm5  12679  rpexp1i  12691  sqrt2irr  12699  nonsq  12744  eulerthlemrprm  12766  eulerthlema  12767  phisum  12778  modprmn0modprm0  12794  pclemdc  12826  pcz  12870  pcmpt  12881  fldivp1  12886  pcfac  12888  expnprm  12891  oddprmdvds  12892  prmpwdvds  12893  infpnlem1  12897  1arith  12905  4sqlem2  12927  4sqlemafi  12933  4sqleminfi  12935  4sqexercise2  12937  4sqlemsdc  12938  ctinfom  13014  enctlem  13018  nninfdclemlt  13037  setsfun  13082  setsfun0  13083  setscom  13087  gsumfzval  13439  mndissubm  13523  resmhm  13535  resmhm2  13536  mhmco  13538  gsumfzz  13543  gsumwsubmcl  13544  gsumwmhm  13546  dfgrp2  13575  isgrpinv  13602  mulgval  13674  mulgnnp1  13682  mulgz  13702  grpissubg  13746  resghm  13812  qusecsub  13883  isrng  13912  lmodfopne  14305  dflidl2rng  14460  gsumfzfsumlemm  14566  mulgrhm2  14589  znidomb  14637  znunit  14638  psrbaglesuppg  14651  psrbagfi  14652  tgdom  14761  ssrest  14871  cnfval  14883  cnpfval  14884  cnpval  14887  iscnp3  14892  ssidcn  14899  cnpnei  14908  cnntr  14914  cncnp  14919  cnptopresti  14927  tx1cn  14958  upxp  14961  imasnopn  14988  bdmet  15191  metcnp  15201  ivthinclemlr  15326  ivthinclemur  15328  ivthinc  15332  dvrecap  15402  dvmptfsum  15414  elply2  15424  plymullem1  15437  plycolemc  15447  plycjlemc  15449  dvply1  15454  pilem3  15472  relogeftb  15554  logbgcd1irr  15656  mpodvdsmulf1o  15679  mersenne  15686  lgslem4  15697  lgsval  15698  lgsfvalg  15699  lgsval2lem  15704  lgsmod  15720  lgsdir2lem4  15725  lgsdinn0  15742  lgsquad2lem2  15776  lgsquad3  15778  2lgslem1c  15784  2sqlem6  15814  2sqlem7  15815  isupgren  15910  wrdupgren  15911  isumgren  15920  wrdumgren  15921  isuspgren  15970  isusgren  15971  2omap  16418  pw1map  16420  nnsf  16431  peano4nninf  16432  nninfalllem1  16434  nninfsellemqall  16441  nninfsellemeqinf  16442  nninffeq  16446  exmidsbthrlem  16450  isomninnlem  16458  iswomninnlem  16477  iswomni0  16479  ismkvnnlem  16480