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  529  simplrl  537  simplrr  538  ordtri2or2exmidlem  4648  en2lp  4676  foun  5633  f1oprg  5660  fcof1o  5962  foeqcnvco  5963  f1eqcocnv  5964  caovord3  6228  f1o2ndf1  6424  suppfnss  6457  suppssdc  6460  suppssfvg  6463  smores2  6525  frecrdg  6639  nnaordex  6761  xpdom2  7082  xpen  7098  mapen  7099  xpmapenlem  7102  nndomo  7118  phpm  7120  fidifsnen  7125  isinfinf  7154  fidcen  7156  finexdc  7160  elssdc  7162  fientri3  7175  fiintim  7191  xpfi  7192  f1dmvrnfibi  7211  sbthlemi8  7234  2omap  7269  2omapfi  7271  djudom  7384  omp1eomlem  7385  difinfsn  7391  ctmlemr  7399  ctssdccl  7402  nnnninfeq  7419  enomnilem  7429  finomni  7431  ismkvnex  7446  enmkvlem  7452  nninfwlpoimlemginf  7467  exmidfodomrlemrALT  7506  exmidontriim  7532  netap  7568  exmidapne  7574  acnccim  7586  dfplpq2  7669  recclnq  7707  subhalfnqq  7729  distrnq0  7774  prarloclem3step  7811  genpml  7832  genpmu  7833  addnqprl  7844  addnqpru  7845  appdivnq  7878  mulnqprl  7883  mulnqpru  7884  mullocpr  7886  ltexprlemfl  7924  ltexprlemfu  7926  ltmprr  7957  archpr  7958  cauappcvgprlemm  7960  caucvgprlemladdrl  7993  caucvgprprlemopl  8012  caucvgprprlemopu  8014  recexgt0sr  8088  mulgt0sr  8093  elrealeu  8144  axcaucvglemcau  8213  axcaucvglemres  8214  cnegex  8451  apirr  8879  mulge0  8893  lemul12a  9136  lediv2a  9169  creur  9233  nndiv  9278  zaddcllemneg  9616  peano5uzti  9686  supinfneg  9927  infsupneg  9928  divfnzn  9953  xrltso  10129  xpncan  10204  xltadd1  10209  xleaddadd  10220  elioc2  10269  elico2  10270  elicc2  10271  exfzdc  10586  zsupcllemstep  10589  infssuzex  10593  suprzubdc  10596  exbtwnzlemex  10609  rebtwn2z  10614  modqid  10711  modqcyc  10721  mulqaddmodid  10726  modqadd2mod  10736  addmodlteq  10760  frecuzrdgg  10778  nninfinf  10805  seq3val  10822  seqvalcd  10823  seq3clss  10833  iseqf1olemqcl  10861  iseqf1olemnab  10863  seq3f1olemp  10877  seq3f1o  10879  seqf1oglem1  10881  seqfeq4g  10893  fser0const  10897  ser3ge0  10898  exp3vallem  10902  qsqeqor  11012  facndiv  11101  faclbnd  11103  bcval5  11125  hashen  11147  fihashdom  11167  hashunlem  11168  hashfacen  11208  zfz1isolemiso  11211  seq3coll  11214  ccatsymb  11290  ccatrn  11297  ccatw2s1p2  11334  swrdccatin1  11417  swrdccatin2  11421  swrdccat3b  11432  caucvgre  11666  resqrexlemlo  11698  cau3lem  11799  qdenre  11887  rexico  11906  fimaxre2  11912  2zinfmin  11928  xrmaxiflemcl  11930  xrmaxifle  11931  xrmaxiflemcom  11934  2clim  11986  cn1lem  11999  climsqz  12020  climsqz2  12021  climcau  12032  sumrbdclem  12063  summodclem2a  12067  fsum3  12073  fsumcl2lem  12084  fsumadd  12092  sumsnf  12095  fsum2dlemstep  12120  fisum0diag2  12133  fsummulc2  12134  mertenslemub  12220  mertenslemi1  12221  mertensabs  12223  ntrivcvgap  12234  prodrbdclem  12257  prodmodclem3  12261  prodmodclem2a  12262  prodmodc  12264  prod1dc  12272  prodsnf  12278  fprod2dlemstep  12308  efaddlem  12360  tanaddaplem  12424  zdvdsdc  12498  dvdseq  12534  dvdsext  12541  odd2np1  12559  sqoddm1div8z  12572  nno  12592  dfgcd3  12706  nninfctlemfo  12736  dvdslcm  12766  lcmneg  12771  lcmgcdlem  12774  ncoprmgcdne1b  12786  qredeq  12793  qredeu  12794  divgcdcoprm0  12798  exprmfct  12835  prmdvdsfz  12836  isprm5  12839  rpexp1i  12851  sqrt2irr  12859  nonsq  12904  eulerthlemrprm  12926  eulerthlema  12927  phisum  12938  modprmn0modprm0  12954  pclemdc  12986  pcz  13030  pcmpt  13041  fldivp1  13046  pcfac  13048  expnprm  13051  oddprmdvds  13052  prmpwdvds  13053  infpnlem1  13057  1arith  13065  4sqlem2  13087  4sqlemafi  13093  4sqleminfi  13095  4sqexercise2  13097  4sqlemsdc  13098  ctinfom  13179  enctlem  13183  nninfdclemlt  13202  setsfun  13247  setsfun0  13248  setscom  13252  gsumfzval  13604  mndissubm  13688  resmhm  13700  resmhm2  13701  mhmco  13703  gsumfzz  13708  gsumwsubmcl  13709  gsumwmhm  13711  dfgrp2  13740  isgrpinv  13767  mulgval  13839  mulgnnp1  13847  mulgz  13867  grpissubg  13911  resghm  13977  qusecsub  14048  isrng  14078  lmodfopne  14474  dflidl2rng  14629  gsumfzfsumlemm  14735  mulgrhm2  14758  znidomb  14806  znunit  14807  psrbaglesuppg  14821  psrbagfi  14823  tgdom  14937  ssrest  15047  cnfval  15059  cnpfval  15060  cnpval  15063  iscnp3  15068  ssidcn  15075  cnpnei  15084  cnntr  15090  cncnp  15095  cnptopresti  15103  tx1cn  15134  upxp  15137  imasnopn  15164  bdmet  15367  metcnp  15377  ivthinclemlr  15502  ivthinclemur  15504  ivthinc  15508  dvrecap  15578  dvmptfsum  15590  elply2  15600  plymullem1  15613  plycolemc  15623  plycjlemc  15625  dvply1  15630  pilem3  15648  relogeftb  15730  logbgcd1irr  15832  mpodvdsmulf1o  15858  mersenne  15865  lgslem4  15876  lgsval  15877  lgsfvalg  15878  lgsval2lem  15883  lgsmod  15899  lgsdir2lem4  15904  lgsdinn0  15921  lgsquad2lem2  15955  lgsquad3  15957  2lgslem1c  15963  2sqlem6  15993  2sqlem7  15994  isupgren  16090  wrdupgren  16091  isumgren  16100  wrdumgren  16101  isuspgren  16152  isusgren  16153  clwwlkext2edg  16417  clwwlknonex2  16434  depindlem3  16503  pw1map  16769  nnsf  16783  peano4nninf  16784  nninfalllem1  16786  nninfsellemqall  16793  nninfsellemeqinf  16794  nninffeq  16798  exmidsbthrlem  16802  isomninnlem  16814  iswomninnlem  16834  iswomni0  16836  ismkvnnlem  16837