Theorem ad2antlr 474

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 271	. 2 |- ( ( ph /\ th ) -> ps )
3	2	adantll 461	1 |- ( ( ( ch /\ ph ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad3antlr  478  simplr  498  simplrl  503  simplrr  504  ordtri2or2exmidlem  4355  en2lp  4383  xpid11m  4671  foun  5285  f1oprg  5308  fcof1o  5582  foeqcnvco  5583  f1eqcocnv  5584  caovord3  5832  f1o2ndf1  6007  smores2  6073  frecrdg  6187  nnaordex  6300  xpdom2  6601  xpen  6615  mapen  6616  xpmapenlem  6619  nndomo  6634  phpm  6635  fidifsnen  6640  isinfinf  6667  finexdc  6672  fientri3  6679  fiintim  6693  xpfi  6694  f1dmvrnfibi  6707  sbthlemi8  6727  djudom  6836  enomnilem  6848  finomni  6850  exmidfodomrlemrALT  6883  dfplpq2  6967  recclnq  7005  subhalfnqq  7027  distrnq0  7072  prarloclem3step  7109  genpml  7130  genpmu  7131  addnqprl  7142  addnqpru  7143  appdivnq  7176  mulnqprl  7181  mulnqpru  7182  mullocpr  7184  ltexprlemfl  7222  ltexprlemfu  7224  ltmprr  7255  archpr  7256  cauappcvgprlemm  7258  caucvgprlemladdrl  7291  caucvgprprlemopl  7310  caucvgprprlemopu  7312  recexgt0sr  7373  mulgt0sr  7377  elrealeu  7421  axcaucvglemcau  7487  axcaucvglemres  7488  cnegex  7714  apirr  8136  mulge0  8150  lemul12a  8377  lediv2a  8410  creur  8473  nndiv  8517  zaddcllemneg  8843  peano5uzti  8908  supinfneg  9137  infsupneg  9138  divfnzn  9160  xrltso  9320  elioc2  9408  elico2  9409  elicc2  9410  exfzdc  9705  exbtwnzlemex  9715  rebtwn2z  9720  modqid  9810  modqcyc  9820  mulqaddmodid  9825  modqadd2mod  9835  addmodlteq  9859  frecuzrdgg  9877  iseqvalt  9927  seq3val  9928  iseqoveq  9939  seq3clss  9941  iseqf1olemqcl  9969  iseqf1olemnab  9971  seq3f1olemp  9985  seq3f1o  9987  fser0const  10005  ser3ge0  10006  exp3vallem  10010  facndiv  10201  faclbnd  10203  ibcval5  10225  hashen  10246  fihashdom  10265  hashunlem  10266  hashfacen  10295  zfz1isolemiso  10298  iseqcoll  10301  caucvgre  10468  resqrexlemlo  10500  cau3lem  10601  qdenre  10689  rexico  10708  fimaxre2  10712  2clim  10743  cn1lem  10756  climsqz  10777  climsqz2  10778  climcau  10790  isumrblem  10819  isummolem2a  10825  fisum  10832  fsum3  10833  fsumcl2lem  10846  fsumadd  10854  sumsnf  10857  fsum2dlemstep  10882  fisum0diag2  10895  fsummulc2  10896  mertenslemub  10982  mertenslemi1  10983  mertensabs  10985  efaddlem  11018  tanaddaplem  11083  zdvdsdc  11149  dvdseq  11181  dvdsext  11188  odd2np1  11205  sqoddm1div8z  11218  nno  11238  zsupcllemstep  11273  infssuzex  11277  dfgcd3  11331  dvdslcm  11383  lcmneg  11388  lcmgcdlem  11391  ncoprmgcdne1b  11403  qredeq  11410  qredeu  11411  divgcdcoprm0  11415  exprmfct  11451  prmdvdsfz  11452  rpexp1i  11465  sqrt2irr  11473  nonsq  11517  setsfun  11583  setsfun0  11584  setscom  11588  tgdom  11826  nnsf  12161  peano4nninf  12162  nninfalllemn  12164  nninfalllem1  12165  nninfsellemqall  12173  nninfsellemeqinf  12174  exmidsbthrlem  12178