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  4485  en2lp  4513  foun  5433  f1oprg  5458  fcof1o  5739  foeqcnvco  5740  f1eqcocnv  5741  caovord3  5994  f1o2ndf1  6175  smores2  6241  frecrdg  6355  nnaordex  6474  xpdom2  6776  xpen  6790  mapen  6791  xpmapenlem  6794  nndomo  6809  phpm  6810  fidifsnen  6815  isinfinf  6842  finexdc  6847  fientri3  6859  fiintim  6873  xpfi  6874  f1dmvrnfibi  6888  sbthlemi8  6908  djudom  7037  omp1eomlem  7038  difinfsn  7044  ctmlemr  7052  ctssdccl  7055  nnnninfeq  7071  enomnilem  7081  finomni  7083  ismkvnex  7098  enmkvlem  7104  exmidfodomrlemrALT  7138  exmidontriim  7160  dfplpq2  7274  recclnq  7312  subhalfnqq  7334  distrnq0  7379  prarloclem3step  7416  genpml  7437  genpmu  7438  addnqprl  7449  addnqpru  7450  appdivnq  7483  mulnqprl  7488  mulnqpru  7489  mullocpr  7491  ltexprlemfl  7529  ltexprlemfu  7531  ltmprr  7562  archpr  7563  cauappcvgprlemm  7565  caucvgprlemladdrl  7598  caucvgprprlemopl  7617  caucvgprprlemopu  7619  recexgt0sr  7693  mulgt0sr  7698  elrealeu  7749  axcaucvglemcau  7818  axcaucvglemres  7819  cnegex  8053  apirr  8480  mulge0  8494  lemul12a  8733  lediv2a  8766  creur  8830  nndiv  8874  zaddcllemneg  9206  peano5uzti  9272  supinfneg  9506  infsupneg  9507  divfnzn  9530  xrltso  9703  xpncan  9775  xltadd1  9780  xleaddadd  9791  elioc2  9840  elico2  9841  elicc2  9842  exfzdc  10139  exbtwnzlemex  10149  rebtwn2z  10154  modqid  10248  modqcyc  10258  mulqaddmodid  10263  modqadd2mod  10273  addmodlteq  10297  frecuzrdgg  10315  seq3val  10357  seqvalcd  10358  seq3clss  10366  iseqf1olemqcl  10385  iseqf1olemnab  10387  seq3f1olemp  10401  seq3f1o  10403  fser0const  10415  ser3ge0  10416  exp3vallem  10420  facndiv  10613  faclbnd  10615  bcval5  10637  hashen  10658  fihashdom  10677  hashunlem  10678  hashfacen  10707  zfz1isolemiso  10710  seq3coll  10713  caucvgre  10881  resqrexlemlo  10913  cau3lem  11014  qdenre  11102  rexico  11121  fimaxre2  11126  xrmaxiflemcl  11142  xrmaxifle  11143  xrmaxiflemcom  11146  2clim  11198  cn1lem  11211  climsqz  11232  climsqz2  11233  climcau  11244  sumrbdclem  11274  summodclem2a  11278  fsum3  11284  fsumcl2lem  11295  fsumadd  11303  sumsnf  11306  fsum2dlemstep  11331  fisum0diag2  11344  fsummulc2  11345  mertenslemub  11431  mertenslemi1  11432  mertensabs  11434  ntrivcvgap  11445  prodrbdclem  11468  prodmodclem3  11472  prodmodclem2a  11473  prodmodc  11475  prod1dc  11483  prodsnf  11489  fprod2dlemstep  11519  efaddlem  11571  tanaddaplem  11635  zdvdsdc  11707  dvdseq  11739  dvdsext  11746  odd2np1  11763  sqoddm1div8z  11776  nno  11796  zsupcllemstep  11831  infssuzex  11835  dfgcd3  11893  dvdslcm  11945  lcmneg  11950  lcmgcdlem  11953  ncoprmgcdne1b  11965  qredeq  11972  qredeu  11973  divgcdcoprm0  11977  exprmfct  12014  prmdvdsfz  12015  rpexp1i  12028  sqrt2irr  12036  nonsq  12081  eulerthlemrprm  12103  eulerthlema  12104  phisum  12114  ctinfom  12157  enctlem  12161  nninfdclemlt  12182  setsfun  12225  setsfun0  12226  setscom  12230  tgdom  12472  ssrest  12582  cnfval  12594  cnpfval  12595  cnpval  12598  iscnp3  12603  ssidcn  12610  cnpnei  12619  cnntr  12625  cncnp  12630  cnptopresti  12638  tx1cn  12669  upxp  12672  imasnopn  12699  bdmet  12902  metcnp  12912  ivthinclemlr  13015  ivthinclemur  13017  ivthinc  13021  dvrecap  13077  pilem3  13104  relogeftb  13186  logbgcd1irr  13284  nnsf  13577  peano4nninf  13578  nninfalllem1  13580  nninfsellemqall  13587  nninfsellemeqinf  13588  nninffeq  13592  exmidsbthrlem  13593  isomninnlem  13601  iswomninnlem  13620  iswomni0  13622  ismkvnnlem  13623