Theorem ad2antlr 481

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  ad3antlr  485  simplr  520  simplrl  525  simplrr  526  ordtri2or2exmidlem  4502  en2lp  4530  foun  5450  f1oprg  5475  fcof1o  5756  foeqcnvco  5757  f1eqcocnv  5758  caovord3  6011  f1o2ndf1  6192  smores2  6258  frecrdg  6372  nnaordex  6491  xpdom2  6793  xpen  6807  mapen  6808  xpmapenlem  6811  nndomo  6826  phpm  6827  fidifsnen  6832  isinfinf  6859  finexdc  6864  fientri3  6876  fiintim  6890  xpfi  6891  f1dmvrnfibi  6905  sbthlemi8  6925  djudom  7054  omp1eomlem  7055  difinfsn  7061  ctmlemr  7069  ctssdccl  7072  nnnninfeq  7088  enomnilem  7098  finomni  7100  ismkvnex  7115  enmkvlem  7121  exmidfodomrlemrALT  7155  exmidontriim  7177  dfplpq2  7291  recclnq  7329  subhalfnqq  7351  distrnq0  7396  prarloclem3step  7433  genpml  7454  genpmu  7455  addnqprl  7466  addnqpru  7467  appdivnq  7500  mulnqprl  7505  mulnqpru  7506  mullocpr  7508  ltexprlemfl  7546  ltexprlemfu  7548  ltmprr  7579  archpr  7580  cauappcvgprlemm  7582  caucvgprlemladdrl  7615  caucvgprprlemopl  7634  caucvgprprlemopu  7636  recexgt0sr  7710  mulgt0sr  7715  elrealeu  7766  axcaucvglemcau  7835  axcaucvglemres  7836  cnegex  8072  apirr  8499  mulge0  8513  lemul12a  8753  lediv2a  8786  creur  8850  nndiv  8894  zaddcllemneg  9226  peano5uzti  9295  supinfneg  9529  infsupneg  9530  divfnzn  9555  xrltso  9728  xpncan  9803  xltadd1  9808  xleaddadd  9819  elioc2  9868  elico2  9869  elicc2  9870  exfzdc  10171  exbtwnzlemex  10181  rebtwn2z  10186  modqid  10280  modqcyc  10290  mulqaddmodid  10295  modqadd2mod  10305  addmodlteq  10329  frecuzrdgg  10347  seq3val  10389  seqvalcd  10390  seq3clss  10398  iseqf1olemqcl  10417  iseqf1olemnab  10419  seq3f1olemp  10433  seq3f1o  10435  fser0const  10447  ser3ge0  10448  exp3vallem  10452  qsqeqor  10561  facndiv  10648  faclbnd  10650  bcval5  10672  hashen  10693  fihashdom  10712  hashunlem  10713  hashfacen  10745  zfz1isolemiso  10748  seq3coll  10751  caucvgre  10919  resqrexlemlo  10951  cau3lem  11052  qdenre  11140  rexico  11159  fimaxre2  11164  2zinfmin  11180  xrmaxiflemcl  11182  xrmaxifle  11183  xrmaxiflemcom  11186  2clim  11238  cn1lem  11251  climsqz  11272  climsqz2  11273  climcau  11284  sumrbdclem  11314  summodclem2a  11318  fsum3  11324  fsumcl2lem  11335  fsumadd  11343  sumsnf  11346  fsum2dlemstep  11371  fisum0diag2  11384  fsummulc2  11385  mertenslemub  11471  mertenslemi1  11472  mertensabs  11474  ntrivcvgap  11485  prodrbdclem  11508  prodmodclem3  11512  prodmodclem2a  11513  prodmodc  11515  prod1dc  11523  prodsnf  11529  fprod2dlemstep  11559  efaddlem  11611  tanaddaplem  11675  zdvdsdc  11748  dvdseq  11782  dvdsext  11789  odd2np1  11806  sqoddm1div8z  11819  nno  11839  zsupcllemstep  11874  infssuzex  11878  suprzubdc  11881  dfgcd3  11939  dvdslcm  11997  lcmneg  12002  lcmgcdlem  12005  ncoprmgcdne1b  12017  qredeq  12024  qredeu  12025  divgcdcoprm0  12029  exprmfct  12066  prmdvdsfz  12067  isprm5  12070  rpexp1i  12082  sqrt2irr  12090  nonsq  12135  eulerthlemrprm  12157  eulerthlema  12158  phisum  12168  modprmn0modprm0  12184  pclemdc  12216  pcz  12259  pcmpt  12269  fldivp1  12274  pcfac  12276  expnprm  12279  oddprmdvds  12280  prmpwdvds  12281  infpnlem1  12285  1arith  12293  4sqlem2  12315  ctinfom  12357  enctlem  12361  nninfdclemlt  12380  setsfun  12425  setsfun0  12426  setscom  12430  tgdom  12672  ssrest  12782  cnfval  12794  cnpfval  12795  cnpval  12798  iscnp3  12803  ssidcn  12810  cnpnei  12819  cnntr  12825  cncnp  12830  cnptopresti  12838  tx1cn  12869  upxp  12872  imasnopn  12899  bdmet  13102  metcnp  13112  ivthinclemlr  13215  ivthinclemur  13217  ivthinc  13221  dvrecap  13277  pilem3  13304  relogeftb  13386  logbgcd1irr  13485  lgslem4  13504  lgsval  13505  lgsfvalg  13506  lgsval2lem  13511  lgsmod  13527  lgsdir2lem4  13532  lgsdinn0  13549  2sqlem6  13556  2sqlem7  13557  nnsf  13845  peano4nninf  13846  nninfalllem1  13848  nninfsellemqall  13855  nninfsellemeqinf  13856  nninffeq  13860  exmidsbthrlem  13861  isomninnlem  13869  iswomninnlem  13888  iswomni0  13890  ismkvnnlem  13891