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  8134  apirr  8561  mulge0  8575  lemul12a  8818  lediv2a  8851  creur  8915  nndiv  8959  zaddcllemneg  9291  peano5uzti  9360  supinfneg  9594  infsupneg  9595  divfnzn  9620  xrltso  9795  xpncan  9870  xltadd1  9875  xleaddadd  9886  elioc2  9935  elico2  9936  elicc2  9937  exfzdc  10239  exbtwnzlemex  10249  rebtwn2z  10254  modqid  10348  modqcyc  10358  mulqaddmodid  10363  modqadd2mod  10373  addmodlteq  10397  frecuzrdgg  10415  seq3val  10457  seqvalcd  10458  seq3clss  10466  iseqf1olemqcl  10485  iseqf1olemnab  10487  seq3f1olemp  10501  seq3f1o  10503  fser0const  10515  ser3ge0  10516  exp3vallem  10520  qsqeqor  10630  facndiv  10718  faclbnd  10720  bcval5  10742  hashen  10763  fihashdom  10782  hashunlem  10783  hashfacen  10815  zfz1isolemiso  10818  seq3coll  10821  caucvgre  10989  resqrexlemlo  11021  cau3lem  11122  qdenre  11210  rexico  11229  fimaxre2  11234  2zinfmin  11250  xrmaxiflemcl  11252  xrmaxifle  11253  xrmaxiflemcom  11256  2clim  11308  cn1lem  11321  climsqz  11342  climsqz2  11343  climcau  11354  sumrbdclem  11384  summodclem2a  11388  fsum3  11394  fsumcl2lem  11405  fsumadd  11413  sumsnf  11416  fsum2dlemstep  11441  fisum0diag2  11454  fsummulc2  11455  mertenslemub  11541  mertenslemi1  11542  mertensabs  11544  ntrivcvgap  11555  prodrbdclem  11578  prodmodclem3  11582  prodmodclem2a  11583  prodmodc  11585  prod1dc  11593  prodsnf  11599  fprod2dlemstep  11629  efaddlem  11681  tanaddaplem  11745  zdvdsdc  11818  dvdseq  11853  dvdsext  11860  odd2np1  11877  sqoddm1div8z  11890  nno  11910  zsupcllemstep  11945  infssuzex  11949  suprzubdc  11952  dfgcd3  12010  dvdslcm  12068  lcmneg  12073  lcmgcdlem  12076  ncoprmgcdne1b  12088  qredeq  12095  qredeu  12096  divgcdcoprm0  12100  exprmfct  12137  prmdvdsfz  12138  isprm5  12141  rpexp1i  12153  sqrt2irr  12161  nonsq  12206  eulerthlemrprm  12228  eulerthlema  12229  phisum  12239  modprmn0modprm0  12255  pclemdc  12287  pcz  12330  pcmpt  12340  fldivp1  12345  pcfac  12347  expnprm  12350  oddprmdvds  12351  prmpwdvds  12352  infpnlem1  12356  1arith  12364  4sqlem2  12386  ctinfom  12428  enctlem  12432  nninfdclemlt  12451  setsfun  12496  setsfun0  12497  setscom  12501  mndissubm  12865  mhmco  12873  dfgrp2  12901  isgrpinv  12925  mulgval  12985  mulgnnp1  12990  mulgz  13009  grpissubg  13052  tgdom  13542  ssrest  13652  cnfval  13664  cnpfval  13665  cnpval  13668  iscnp3  13673  ssidcn  13680  cnpnei  13689  cnntr  13695  cncnp  13700  cnptopresti  13708  tx1cn  13739  upxp  13742  imasnopn  13769  bdmet  13972  metcnp  13982  ivthinclemlr  14085  ivthinclemur  14087  ivthinc  14091  dvrecap  14147  pilem3  14174  relogeftb  14256  logbgcd1irr  14355  lgslem4  14374  lgsval  14375  lgsfvalg  14376  lgsval2lem  14381  lgsmod  14397  lgsdir2lem4  14402  lgsdinn0  14419  2sqlem6  14437  2sqlem7  14438  nnsf  14724  peano4nninf  14725  nninfalllem1  14727  nninfsellemqall  14734  nninfsellemeqinf  14735  nninffeq  14739  exmidsbthrlem  14740  isomninnlem  14748  iswomninnlem  14767  iswomni0  14769  ismkvnnlem  14770