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  4617  en2lp  4645  foun  5590  f1oprg  5616  fcof1o  5912  foeqcnvco  5913  f1eqcocnv  5914  caovord3  6178  f1o2ndf1  6372  smores2  6438  frecrdg  6552  nnaordex  6672  xpdom2  6986  xpen  7002  mapen  7003  xpmapenlem  7006  nndomo  7021  phpm  7023  fidifsnen  7028  isinfinf  7055  finexdc  7060  fientri3  7073  fiintim  7089  xpfi  7090  f1dmvrnfibi  7107  sbthlemi8  7127  djudom  7256  omp1eomlem  7257  difinfsn  7263  ctmlemr  7271  ctssdccl  7274  nnnninfeq  7291  enomnilem  7301  finomni  7303  ismkvnex  7318  enmkvlem  7324  nninfwlpoimlemginf  7339  exmidfodomrlemrALT  7377  exmidontriim  7403  netap  7436  exmidapne  7442  acnccim  7454  dfplpq2  7537  recclnq  7575  subhalfnqq  7597  distrnq0  7642  prarloclem3step  7679  genpml  7700  genpmu  7701  addnqprl  7712  addnqpru  7713  appdivnq  7746  mulnqprl  7751  mulnqpru  7752  mullocpr  7754  ltexprlemfl  7792  ltexprlemfu  7794  ltmprr  7825  archpr  7826  cauappcvgprlemm  7828  caucvgprlemladdrl  7861  caucvgprprlemopl  7880  caucvgprprlemopu  7882  recexgt0sr  7956  mulgt0sr  7961  elrealeu  8012  axcaucvglemcau  8081  axcaucvglemres  8082  cnegex  8320  apirr  8748  mulge0  8762  lemul12a  9005  lediv2a  9038  creur  9102  nndiv  9147  zaddcllemneg  9481  peano5uzti  9551  supinfneg  9786  infsupneg  9787  divfnzn  9812  xrltso  9988  xpncan  10063  xltadd1  10068  xleaddadd  10079  elioc2  10128  elico2  10129  elicc2  10130  exfzdc  10441  zsupcllemstep  10444  infssuzex  10448  suprzubdc  10451  exbtwnzlemex  10464  rebtwn2z  10469  modqid  10566  modqcyc  10576  mulqaddmodid  10581  modqadd2mod  10591  addmodlteq  10615  frecuzrdgg  10633  nninfinf  10660  seq3val  10677  seqvalcd  10678  seq3clss  10688  iseqf1olemqcl  10716  iseqf1olemnab  10718  seq3f1olemp  10732  seq3f1o  10734  seqf1oglem1  10736  seqfeq4g  10748  fser0const  10752  ser3ge0  10753  exp3vallem  10757  qsqeqor  10867  facndiv  10956  faclbnd  10958  bcval5  10980  hashen  11001  fihashdom  11020  hashunlem  11021  hashfacen  11053  zfz1isolemiso  11056  seq3coll  11059  ccatsymb  11132  ccatrn  11139  ccatw2s1p2  11171  swrdccatin1  11252  swrdccatin2  11256  swrdccat3b  11267  caucvgre  11487  resqrexlemlo  11519  cau3lem  11620  qdenre  11708  rexico  11727  fimaxre2  11733  2zinfmin  11749  xrmaxiflemcl  11751  xrmaxifle  11752  xrmaxiflemcom  11755  2clim  11807  cn1lem  11820  climsqz  11841  climsqz2  11842  climcau  11853  sumrbdclem  11883  summodclem2a  11887  fsum3  11893  fsumcl2lem  11904  fsumadd  11912  sumsnf  11915  fsum2dlemstep  11940  fisum0diag2  11953  fsummulc2  11954  mertenslemub  12040  mertenslemi1  12041  mertensabs  12043  ntrivcvgap  12054  prodrbdclem  12077  prodmodclem3  12081  prodmodclem2a  12082  prodmodc  12084  prod1dc  12092  prodsnf  12098  fprod2dlemstep  12128  efaddlem  12180  tanaddaplem  12244  zdvdsdc  12318  dvdseq  12354  dvdsext  12361  odd2np1  12379  sqoddm1div8z  12392  nno  12412  dfgcd3  12526  nninfctlemfo  12556  dvdslcm  12586  lcmneg  12591  lcmgcdlem  12594  ncoprmgcdne1b  12606  qredeq  12613  qredeu  12614  divgcdcoprm0  12618  exprmfct  12655  prmdvdsfz  12656  isprm5  12659  rpexp1i  12671  sqrt2irr  12679  nonsq  12724  eulerthlemrprm  12746  eulerthlema  12747  phisum  12758  modprmn0modprm0  12774  pclemdc  12806  pcz  12850  pcmpt  12861  fldivp1  12866  pcfac  12868  expnprm  12871  oddprmdvds  12872  prmpwdvds  12873  infpnlem1  12877  1arith  12885  4sqlem2  12907  4sqlemafi  12913  4sqleminfi  12915  4sqexercise2  12917  4sqlemsdc  12918  ctinfom  12994  enctlem  12998  nninfdclemlt  13017  setsfun  13062  setsfun0  13063  setscom  13067  gsumfzval  13419  mndissubm  13503  resmhm  13515  resmhm2  13516  mhmco  13518  gsumfzz  13523  gsumwsubmcl  13524  gsumwmhm  13526  dfgrp2  13555  isgrpinv  13582  mulgval  13654  mulgnnp1  13662  mulgz  13682  grpissubg  13726  resghm  13792  qusecsub  13863  isrng  13892  lmodfopne  14284  dflidl2rng  14439  gsumfzfsumlemm  14545  mulgrhm2  14568  znidomb  14616  znunit  14617  psrbaglesuppg  14630  psrbagfi  14631  tgdom  14740  ssrest  14850  cnfval  14862  cnpfval  14863  cnpval  14866  iscnp3  14871  ssidcn  14878  cnpnei  14887  cnntr  14893  cncnp  14898  cnptopresti  14906  tx1cn  14937  upxp  14940  imasnopn  14967  bdmet  15170  metcnp  15180  ivthinclemlr  15305  ivthinclemur  15307  ivthinc  15311  dvrecap  15381  dvmptfsum  15393  elply2  15403  plymullem1  15416  plycolemc  15426  plycjlemc  15428  dvply1  15433  pilem3  15451  relogeftb  15533  logbgcd1irr  15635  mpodvdsmulf1o  15658  mersenne  15665  lgslem4  15676  lgsval  15677  lgsfvalg  15678  lgsval2lem  15683  lgsmod  15699  lgsdir2lem4  15704  lgsdinn0  15721  lgsquad2lem2  15755  lgsquad3  15757  2lgslem1c  15763  2sqlem6  15793  2sqlem7  15794  isupgren  15889  wrdupgren  15890  isumgren  15899  wrdumgren  15900  isuspgren  15949  isusgren  15950  2omap  16318  pw1map  16320  nnsf  16330  peano4nninf  16331  nninfalllem1  16333  nninfsellemqall  16340  nninfsellemeqinf  16341  nninffeq  16345  exmidsbthrlem  16349  isomninnlem  16357  iswomninnlem  16376  iswomni0  16378  ismkvnnlem  16379