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  4574  en2lp  4602  foun  5541  f1oprg  5566  fcof1o  5858  foeqcnvco  5859  f1eqcocnv  5860  caovord3  6120  f1o2ndf1  6314  smores2  6380  frecrdg  6494  nnaordex  6614  xpdom2  6926  xpen  6942  mapen  6943  xpmapenlem  6946  nndomo  6961  phpm  6962  fidifsnen  6967  isinfinf  6994  finexdc  6999  fientri3  7012  fiintim  7028  xpfi  7029  f1dmvrnfibi  7046  sbthlemi8  7066  djudom  7195  omp1eomlem  7196  difinfsn  7202  ctmlemr  7210  ctssdccl  7213  nnnninfeq  7230  enomnilem  7240  finomni  7242  ismkvnex  7257  enmkvlem  7263  nninfwlpoimlemginf  7278  exmidfodomrlemrALT  7311  exmidontriim  7337  netap  7366  exmidapne  7372  acnccim  7384  dfplpq2  7467  recclnq  7505  subhalfnqq  7527  distrnq0  7572  prarloclem3step  7609  genpml  7630  genpmu  7631  addnqprl  7642  addnqpru  7643  appdivnq  7676  mulnqprl  7681  mulnqpru  7682  mullocpr  7684  ltexprlemfl  7722  ltexprlemfu  7724  ltmprr  7755  archpr  7756  cauappcvgprlemm  7758  caucvgprlemladdrl  7791  caucvgprprlemopl  7810  caucvgprprlemopu  7812  recexgt0sr  7886  mulgt0sr  7891  elrealeu  7942  axcaucvglemcau  8011  axcaucvglemres  8012  cnegex  8250  apirr  8678  mulge0  8692  lemul12a  8935  lediv2a  8968  creur  9032  nndiv  9077  zaddcllemneg  9411  peano5uzti  9481  supinfneg  9716  infsupneg  9717  divfnzn  9742  xrltso  9918  xpncan  9993  xltadd1  9998  xleaddadd  10009  elioc2  10058  elico2  10059  elicc2  10060  exfzdc  10369  zsupcllemstep  10372  infssuzex  10376  suprzubdc  10379  exbtwnzlemex  10392  rebtwn2z  10397  modqid  10494  modqcyc  10504  mulqaddmodid  10509  modqadd2mod  10519  addmodlteq  10543  frecuzrdgg  10561  nninfinf  10588  seq3val  10605  seqvalcd  10606  seq3clss  10616  iseqf1olemqcl  10644  iseqf1olemnab  10646  seq3f1olemp  10660  seq3f1o  10662  seqf1oglem1  10664  seqfeq4g  10676  fser0const  10680  ser3ge0  10681  exp3vallem  10685  qsqeqor  10795  facndiv  10884  faclbnd  10886  bcval5  10908  hashen  10929  fihashdom  10948  hashunlem  10949  hashfacen  10981  zfz1isolemiso  10984  seq3coll  10987  ccatsymb  11058  ccatrn  11065  ccatw2s1p2  11097  caucvgre  11292  resqrexlemlo  11324  cau3lem  11425  qdenre  11513  rexico  11532  fimaxre2  11538  2zinfmin  11554  xrmaxiflemcl  11556  xrmaxifle  11557  xrmaxiflemcom  11560  2clim  11612  cn1lem  11625  climsqz  11646  climsqz2  11647  climcau  11658  sumrbdclem  11688  summodclem2a  11692  fsum3  11698  fsumcl2lem  11709  fsumadd  11717  sumsnf  11720  fsum2dlemstep  11745  fisum0diag2  11758  fsummulc2  11759  mertenslemub  11845  mertenslemi1  11846  mertensabs  11848  ntrivcvgap  11859  prodrbdclem  11882  prodmodclem3  11886  prodmodclem2a  11887  prodmodc  11889  prod1dc  11897  prodsnf  11903  fprod2dlemstep  11933  efaddlem  11985  tanaddaplem  12049  zdvdsdc  12123  dvdseq  12159  dvdsext  12166  odd2np1  12184  sqoddm1div8z  12197  nno  12217  dfgcd3  12331  nninfctlemfo  12361  dvdslcm  12391  lcmneg  12396  lcmgcdlem  12399  ncoprmgcdne1b  12411  qredeq  12418  qredeu  12419  divgcdcoprm0  12423  exprmfct  12460  prmdvdsfz  12461  isprm5  12464  rpexp1i  12476  sqrt2irr  12484  nonsq  12529  eulerthlemrprm  12551  eulerthlema  12552  phisum  12563  modprmn0modprm0  12579  pclemdc  12611  pcz  12655  pcmpt  12666  fldivp1  12671  pcfac  12673  expnprm  12676  oddprmdvds  12677  prmpwdvds  12678  infpnlem1  12682  1arith  12690  4sqlem2  12712  4sqlemafi  12718  4sqleminfi  12720  4sqexercise2  12722  4sqlemsdc  12723  ctinfom  12799  enctlem  12803  nninfdclemlt  12822  setsfun  12867  setsfun0  12868  setscom  12872  gsumfzval  13223  mndissubm  13307  resmhm  13319  resmhm2  13320  mhmco  13322  gsumfzz  13327  gsumwsubmcl  13328  gsumwmhm  13330  dfgrp2  13359  isgrpinv  13386  mulgval  13458  mulgnnp1  13466  mulgz  13486  grpissubg  13530  resghm  13596  qusecsub  13667  isrng  13696  lmodfopne  14088  dflidl2rng  14243  gsumfzfsumlemm  14349  mulgrhm2  14372  znidomb  14420  znunit  14421  psrbaglesuppg  14434  psrbagfi  14435  tgdom  14544  ssrest  14654  cnfval  14666  cnpfval  14667  cnpval  14670  iscnp3  14675  ssidcn  14682  cnpnei  14691  cnntr  14697  cncnp  14702  cnptopresti  14710  tx1cn  14741  upxp  14744  imasnopn  14771  bdmet  14974  metcnp  14984  ivthinclemlr  15109  ivthinclemur  15111  ivthinc  15115  dvrecap  15185  dvmptfsum  15197  elply2  15207  plymullem1  15220  plycolemc  15230  plycjlemc  15232  dvply1  15237  pilem3  15255  relogeftb  15337  logbgcd1irr  15439  mpodvdsmulf1o  15462  mersenne  15469  lgslem4  15480  lgsval  15481  lgsfvalg  15482  lgsval2lem  15487  lgsmod  15503  lgsdir2lem4  15508  lgsdinn0  15525  lgsquad2lem2  15559  lgsquad3  15561  2lgslem1c  15567  2sqlem6  15597  2sqlem7  15598  2omap  15932  nnsf  15942  peano4nninf  15943  nninfalllem1  15945  nninfsellemqall  15952  nninfsellemeqinf  15953  nninffeq  15957  exmidsbthrlem  15961  isomninnlem  15969  iswomninnlem  15988  iswomni0  15990  ismkvnnlem  15991