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  4525  en2lp  4553  foun  5480  f1oprg  5505  fcof1o  5789  foeqcnvco  5790  f1eqcocnv  5791  caovord3  6047  f1o2ndf1  6228  smores2  6294  frecrdg  6408  nnaordex  6528  xpdom2  6830  xpen  6844  mapen  6845  xpmapenlem  6848  nndomo  6863  phpm  6864  fidifsnen  6869  isinfinf  6896  finexdc  6901  fientri3  6913  fiintim  6927  xpfi  6928  f1dmvrnfibi  6942  sbthlemi8  6962  djudom  7091  omp1eomlem  7092  difinfsn  7098  ctmlemr  7106  ctssdccl  7109  nnnninfeq  7125  enomnilem  7135  finomni  7137  ismkvnex  7152  enmkvlem  7158  nninfwlpoimlemginf  7173  exmidfodomrlemrALT  7201  exmidontriim  7223  netap  7252  exmidapne  7258  dfplpq2  7352  recclnq  7390  subhalfnqq  7412  distrnq0  7457  prarloclem3step  7494  genpml  7515  genpmu  7516  addnqprl  7527  addnqpru  7528  appdivnq  7561  mulnqprl  7566  mulnqpru  7567  mullocpr  7569  ltexprlemfl  7607  ltexprlemfu  7609  ltmprr  7640  archpr  7641  cauappcvgprlemm  7643  caucvgprlemladdrl  7676  caucvgprprlemopl  7695  caucvgprprlemopu  7697  recexgt0sr  7771  mulgt0sr  7776  elrealeu  7827  axcaucvglemcau  7896  axcaucvglemres  7897  cnegex  8133  apirr  8560  mulge0  8574  lemul12a  8817  lediv2a  8850  creur  8914  nndiv  8958  zaddcllemneg  9290  peano5uzti  9359  supinfneg  9593  infsupneg  9594  divfnzn  9619  xrltso  9794  xpncan  9869  xltadd1  9874  xleaddadd  9885  elioc2  9934  elico2  9935  elicc2  9936  exfzdc  10237  exbtwnzlemex  10247  rebtwn2z  10252  modqid  10346  modqcyc  10356  mulqaddmodid  10361  modqadd2mod  10371  addmodlteq  10395  frecuzrdgg  10413  seq3val  10455  seqvalcd  10456  seq3clss  10464  iseqf1olemqcl  10483  iseqf1olemnab  10485  seq3f1olemp  10499  seq3f1o  10501  fser0const  10513  ser3ge0  10514  exp3vallem  10518  qsqeqor  10627  facndiv  10714  faclbnd  10716  bcval5  10738  hashen  10759  fihashdom  10778  hashunlem  10779  hashfacen  10811  zfz1isolemiso  10814  seq3coll  10817  caucvgre  10985  resqrexlemlo  11017  cau3lem  11118  qdenre  11206  rexico  11225  fimaxre2  11230  2zinfmin  11246  xrmaxiflemcl  11248  xrmaxifle  11249  xrmaxiflemcom  11252  2clim  11304  cn1lem  11317  climsqz  11338  climsqz2  11339  climcau  11350  sumrbdclem  11380  summodclem2a  11384  fsum3  11390  fsumcl2lem  11401  fsumadd  11409  sumsnf  11412  fsum2dlemstep  11437  fisum0diag2  11450  fsummulc2  11451  mertenslemub  11537  mertenslemi1  11538  mertensabs  11540  ntrivcvgap  11551  prodrbdclem  11574  prodmodclem3  11578  prodmodclem2a  11579  prodmodc  11581  prod1dc  11589  prodsnf  11595  fprod2dlemstep  11625  efaddlem  11677  tanaddaplem  11741  zdvdsdc  11814  dvdseq  11848  dvdsext  11855  odd2np1  11872  sqoddm1div8z  11885  nno  11905  zsupcllemstep  11940  infssuzex  11944  suprzubdc  11947  dfgcd3  12005  dvdslcm  12063  lcmneg  12068  lcmgcdlem  12071  ncoprmgcdne1b  12083  qredeq  12090  qredeu  12091  divgcdcoprm0  12095  exprmfct  12132  prmdvdsfz  12133  isprm5  12136  rpexp1i  12148  sqrt2irr  12156  nonsq  12201  eulerthlemrprm  12223  eulerthlema  12224  phisum  12234  modprmn0modprm0  12250  pclemdc  12282  pcz  12325  pcmpt  12335  fldivp1  12340  pcfac  12342  expnprm  12345  oddprmdvds  12346  prmpwdvds  12347  infpnlem1  12351  1arith  12359  4sqlem2  12381  ctinfom  12423  enctlem  12427  nninfdclemlt  12446  setsfun  12491  setsfun0  12492  setscom  12496  mndissubm  12820  mhmco  12828  dfgrp2  12856  isgrpinv  12880  mulgval  12940  mulgnnp1  12945  mulgz  12964  grpissubg  13007  tgdom  13465  ssrest  13575  cnfval  13587  cnpfval  13588  cnpval  13591  iscnp3  13596  ssidcn  13603  cnpnei  13612  cnntr  13618  cncnp  13623  cnptopresti  13631  tx1cn  13662  upxp  13665  imasnopn  13692  bdmet  13895  metcnp  13905  ivthinclemlr  14008  ivthinclemur  14010  ivthinc  14014  dvrecap  14070  pilem3  14097  relogeftb  14179  logbgcd1irr  14278  lgslem4  14297  lgsval  14298  lgsfvalg  14299  lgsval2lem  14304  lgsmod  14320  lgsdir2lem4  14325  lgsdinn0  14342  2sqlem6  14349  2sqlem7  14350  nnsf  14636  peano4nninf  14637  nninfalllem1  14639  nninfsellemqall  14646  nninfsellemeqinf  14647  nninffeq  14651  exmidsbthrlem  14652  isomninnlem  14660  iswomninnlem  14679  iswomni0  14681  ismkvnnlem  14682