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  4562  en2lp  4590  foun  5523  f1oprg  5548  fcof1o  5836  foeqcnvco  5837  f1eqcocnv  5838  caovord3  6097  f1o2ndf1  6286  smores2  6352  frecrdg  6466  nnaordex  6586  xpdom2  6890  xpen  6906  mapen  6907  xpmapenlem  6910  nndomo  6925  phpm  6926  fidifsnen  6931  isinfinf  6958  finexdc  6963  fientri3  6976  fiintim  6992  xpfi  6993  f1dmvrnfibi  7010  sbthlemi8  7030  djudom  7159  omp1eomlem  7160  difinfsn  7166  ctmlemr  7174  ctssdccl  7177  nnnninfeq  7194  enomnilem  7204  finomni  7206  ismkvnex  7221  enmkvlem  7227  nninfwlpoimlemginf  7242  exmidfodomrlemrALT  7270  exmidontriim  7292  netap  7321  exmidapne  7327  dfplpq2  7421  recclnq  7459  subhalfnqq  7481  distrnq0  7526  prarloclem3step  7563  genpml  7584  genpmu  7585  addnqprl  7596  addnqpru  7597  appdivnq  7630  mulnqprl  7635  mulnqpru  7636  mullocpr  7638  ltexprlemfl  7676  ltexprlemfu  7678  ltmprr  7709  archpr  7710  cauappcvgprlemm  7712  caucvgprlemladdrl  7745  caucvgprprlemopl  7764  caucvgprprlemopu  7766  recexgt0sr  7840  mulgt0sr  7845  elrealeu  7896  axcaucvglemcau  7965  axcaucvglemres  7966  cnegex  8204  apirr  8632  mulge0  8646  lemul12a  8889  lediv2a  8922  creur  8986  nndiv  9031  zaddcllemneg  9365  peano5uzti  9434  supinfneg  9669  infsupneg  9670  divfnzn  9695  xrltso  9871  xpncan  9946  xltadd1  9951  xleaddadd  9962  elioc2  10011  elico2  10012  elicc2  10013  exfzdc  10316  zsupcllemstep  10319  infssuzex  10323  suprzubdc  10326  exbtwnzlemex  10339  rebtwn2z  10344  modqid  10441  modqcyc  10451  mulqaddmodid  10456  modqadd2mod  10466  addmodlteq  10490  frecuzrdgg  10508  nninfinf  10535  seq3val  10552  seqvalcd  10553  seq3clss  10563  iseqf1olemqcl  10591  iseqf1olemnab  10593  seq3f1olemp  10607  seq3f1o  10609  seqf1oglem1  10611  seqfeq4g  10623  fser0const  10627  ser3ge0  10628  exp3vallem  10632  qsqeqor  10742  facndiv  10831  faclbnd  10833  bcval5  10855  hashen  10876  fihashdom  10895  hashunlem  10896  hashfacen  10928  zfz1isolemiso  10931  seq3coll  10934  caucvgre  11146  resqrexlemlo  11178  cau3lem  11279  qdenre  11367  rexico  11386  fimaxre2  11392  2zinfmin  11408  xrmaxiflemcl  11410  xrmaxifle  11411  xrmaxiflemcom  11414  2clim  11466  cn1lem  11479  climsqz  11500  climsqz2  11501  climcau  11512  sumrbdclem  11542  summodclem2a  11546  fsum3  11552  fsumcl2lem  11563  fsumadd  11571  sumsnf  11574  fsum2dlemstep  11599  fisum0diag2  11612  fsummulc2  11613  mertenslemub  11699  mertenslemi1  11700  mertensabs  11702  ntrivcvgap  11713  prodrbdclem  11736  prodmodclem3  11740  prodmodclem2a  11741  prodmodc  11743  prod1dc  11751  prodsnf  11757  fprod2dlemstep  11787  efaddlem  11839  tanaddaplem  11903  zdvdsdc  11977  dvdseq  12013  dvdsext  12020  odd2np1  12038  sqoddm1div8z  12051  nno  12071  dfgcd3  12177  nninfctlemfo  12207  dvdslcm  12237  lcmneg  12242  lcmgcdlem  12245  ncoprmgcdne1b  12257  qredeq  12264  qredeu  12265  divgcdcoprm0  12269  exprmfct  12306  prmdvdsfz  12307  isprm5  12310  rpexp1i  12322  sqrt2irr  12330  nonsq  12375  eulerthlemrprm  12397  eulerthlema  12398  phisum  12409  modprmn0modprm0  12425  pclemdc  12457  pcz  12501  pcmpt  12512  fldivp1  12517  pcfac  12519  expnprm  12522  oddprmdvds  12523  prmpwdvds  12524  infpnlem1  12528  1arith  12536  4sqlem2  12558  4sqlemafi  12564  4sqleminfi  12566  4sqexercise2  12568  4sqlemsdc  12569  ctinfom  12645  enctlem  12649  nninfdclemlt  12668  setsfun  12713  setsfun0  12714  setscom  12718  gsumfzval  13034  mndissubm  13107  resmhm  13119  resmhm2  13120  mhmco  13122  gsumfzz  13127  gsumwsubmcl  13128  gsumwmhm  13130  dfgrp2  13159  isgrpinv  13186  mulgval  13252  mulgnnp1  13260  mulgz  13280  grpissubg  13324  resghm  13390  qusecsub  13461  isrng  13490  lmodfopne  13882  dflidl2rng  14037  gsumfzfsumlemm  14143  mulgrhm2  14166  znidomb  14214  znunit  14215  psrbaglesuppg  14226  tgdom  14308  ssrest  14418  cnfval  14430  cnpfval  14431  cnpval  14434  iscnp3  14439  ssidcn  14446  cnpnei  14455  cnntr  14461  cncnp  14466  cnptopresti  14474  tx1cn  14505  upxp  14508  imasnopn  14535  bdmet  14738  metcnp  14748  ivthinclemlr  14873  ivthinclemur  14875  ivthinc  14879  dvrecap  14949  dvmptfsum  14961  elply2  14971  plymullem1  14984  plycolemc  14994  plycjlemc  14996  dvply1  15001  pilem3  15019  relogeftb  15101  logbgcd1irr  15203  mpodvdsmulf1o  15226  mersenne  15233  lgslem4  15244  lgsval  15245  lgsfvalg  15246  lgsval2lem  15251  lgsmod  15267  lgsdir2lem4  15272  lgsdinn0  15289  lgsquad2lem2  15323  lgsquad3  15325  2lgslem1c  15331  2sqlem6  15361  2sqlem7  15362  nnsf  15649  peano4nninf  15650  nninfalllem1  15652  nninfsellemqall  15659  nninfsellemeqinf  15660  nninffeq  15664  exmidsbthrlem  15666  isomninnlem  15674  iswomninnlem  15693  iswomni0  15695  ismkvnnlem  15696