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  4573  en2lp  4601  foun  5540  f1oprg  5565  fcof1o  5857  foeqcnvco  5858  f1eqcocnv  5859  caovord3  6119  f1o2ndf1  6313  smores2  6379  frecrdg  6493  nnaordex  6613  xpdom2  6925  xpen  6941  mapen  6942  xpmapenlem  6945  nndomo  6960  phpm  6961  fidifsnen  6966  isinfinf  6993  finexdc  6998  fientri3  7011  fiintim  7027  xpfi  7028  f1dmvrnfibi  7045  sbthlemi8  7065  djudom  7194  omp1eomlem  7195  difinfsn  7201  ctmlemr  7209  ctssdccl  7212  nnnninfeq  7229  enomnilem  7239  finomni  7241  ismkvnex  7256  enmkvlem  7262  nninfwlpoimlemginf  7277  exmidfodomrlemrALT  7310  exmidontriim  7336  netap  7365  exmidapne  7371  acnccim  7383  dfplpq2  7466  recclnq  7504  subhalfnqq  7526  distrnq0  7571  prarloclem3step  7608  genpml  7629  genpmu  7630  addnqprl  7641  addnqpru  7642  appdivnq  7675  mulnqprl  7680  mulnqpru  7681  mullocpr  7683  ltexprlemfl  7721  ltexprlemfu  7723  ltmprr  7754  archpr  7755  cauappcvgprlemm  7757  caucvgprlemladdrl  7790  caucvgprprlemopl  7809  caucvgprprlemopu  7811  recexgt0sr  7885  mulgt0sr  7890  elrealeu  7941  axcaucvglemcau  8010  axcaucvglemres  8011  cnegex  8249  apirr  8677  mulge0  8691  lemul12a  8934  lediv2a  8967  creur  9031  nndiv  9076  zaddcllemneg  9410  peano5uzti  9480  supinfneg  9715  infsupneg  9716  divfnzn  9741  xrltso  9917  xpncan  9992  xltadd1  9997  xleaddadd  10008  elioc2  10057  elico2  10058  elicc2  10059  exfzdc  10367  zsupcllemstep  10370  infssuzex  10374  suprzubdc  10377  exbtwnzlemex  10390  rebtwn2z  10395  modqid  10492  modqcyc  10502  mulqaddmodid  10507  modqadd2mod  10517  addmodlteq  10541  frecuzrdgg  10559  nninfinf  10586  seq3val  10603  seqvalcd  10604  seq3clss  10614  iseqf1olemqcl  10642  iseqf1olemnab  10644  seq3f1olemp  10658  seq3f1o  10660  seqf1oglem1  10662  seqfeq4g  10674  fser0const  10678  ser3ge0  10679  exp3vallem  10683  qsqeqor  10793  facndiv  10882  faclbnd  10884  bcval5  10906  hashen  10927  fihashdom  10946  hashunlem  10947  hashfacen  10979  zfz1isolemiso  10982  seq3coll  10985  ccatsymb  11056  ccatrn  11063  ccatw2s1p2  11095  caucvgre  11263  resqrexlemlo  11295  cau3lem  11396  qdenre  11484  rexico  11503  fimaxre2  11509  2zinfmin  11525  xrmaxiflemcl  11527  xrmaxifle  11528  xrmaxiflemcom  11531  2clim  11583  cn1lem  11596  climsqz  11617  climsqz2  11618  climcau  11629  sumrbdclem  11659  summodclem2a  11663  fsum3  11669  fsumcl2lem  11680  fsumadd  11688  sumsnf  11691  fsum2dlemstep  11716  fisum0diag2  11729  fsummulc2  11730  mertenslemub  11816  mertenslemi1  11817  mertensabs  11819  ntrivcvgap  11830  prodrbdclem  11853  prodmodclem3  11857  prodmodclem2a  11858  prodmodc  11860  prod1dc  11868  prodsnf  11874  fprod2dlemstep  11904  efaddlem  11956  tanaddaplem  12020  zdvdsdc  12094  dvdseq  12130  dvdsext  12137  odd2np1  12155  sqoddm1div8z  12168  nno  12188  dfgcd3  12302  nninfctlemfo  12332  dvdslcm  12362  lcmneg  12367  lcmgcdlem  12370  ncoprmgcdne1b  12382  qredeq  12389  qredeu  12390  divgcdcoprm0  12394  exprmfct  12431  prmdvdsfz  12432  isprm5  12435  rpexp1i  12447  sqrt2irr  12455  nonsq  12500  eulerthlemrprm  12522  eulerthlema  12523  phisum  12534  modprmn0modprm0  12550  pclemdc  12582  pcz  12626  pcmpt  12637  fldivp1  12642  pcfac  12644  expnprm  12647  oddprmdvds  12648  prmpwdvds  12649  infpnlem1  12653  1arith  12661  4sqlem2  12683  4sqlemafi  12689  4sqleminfi  12691  4sqexercise2  12693  4sqlemsdc  12694  ctinfom  12770  enctlem  12774  nninfdclemlt  12793  setsfun  12838  setsfun0  12839  setscom  12843  gsumfzval  13194  mndissubm  13278  resmhm  13290  resmhm2  13291  mhmco  13293  gsumfzz  13298  gsumwsubmcl  13299  gsumwmhm  13301  dfgrp2  13330  isgrpinv  13357  mulgval  13429  mulgnnp1  13437  mulgz  13457  grpissubg  13501  resghm  13567  qusecsub  13638  isrng  13667  lmodfopne  14059  dflidl2rng  14214  gsumfzfsumlemm  14320  mulgrhm2  14343  znidomb  14391  znunit  14392  psrbaglesuppg  14405  psrbagfi  14406  tgdom  14515  ssrest  14625  cnfval  14637  cnpfval  14638  cnpval  14641  iscnp3  14646  ssidcn  14653  cnpnei  14662  cnntr  14668  cncnp  14673  cnptopresti  14681  tx1cn  14712  upxp  14715  imasnopn  14742  bdmet  14945  metcnp  14955  ivthinclemlr  15080  ivthinclemur  15082  ivthinc  15086  dvrecap  15156  dvmptfsum  15168  elply2  15178  plymullem1  15191  plycolemc  15201  plycjlemc  15203  dvply1  15208  pilem3  15226  relogeftb  15308  logbgcd1irr  15410  mpodvdsmulf1o  15433  mersenne  15440  lgslem4  15451  lgsval  15452  lgsfvalg  15453  lgsval2lem  15458  lgsmod  15474  lgsdir2lem4  15479  lgsdinn0  15496  lgsquad2lem2  15530  lgsquad3  15532  2lgslem1c  15538  2sqlem6  15568  2sqlem7  15569  2omap  15894  nnsf  15904  peano4nninf  15905  nninfalllem1  15907  nninfsellemqall  15914  nninfsellemeqinf  15915  nninffeq  15919  exmidsbthrlem  15923  isomninnlem  15931  iswomninnlem  15950  iswomni0  15952  ismkvnnlem  15953