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  529  simplrl  537  simplrr  538  ordtri2or2exmidlem  4624  en2lp  4652  foun  5602  f1oprg  5629  fcof1o  5930  foeqcnvco  5931  f1eqcocnv  5932  caovord3  6196  f1o2ndf1  6393  smores2  6460  frecrdg  6574  nnaordex  6696  xpdom2  7015  xpen  7031  mapen  7032  xpmapenlem  7035  nndomo  7050  phpm  7052  fidifsnen  7057  isinfinf  7086  fidcen  7088  finexdc  7092  elssdc  7094  fientri3  7107  fiintim  7123  xpfi  7124  f1dmvrnfibi  7143  sbthlemi8  7163  djudom  7292  omp1eomlem  7293  difinfsn  7299  ctmlemr  7307  ctssdccl  7310  nnnninfeq  7327  enomnilem  7337  finomni  7339  ismkvnex  7354  enmkvlem  7360  nninfwlpoimlemginf  7375  exmidfodomrlemrALT  7414  exmidontriim  7440  netap  7473  exmidapne  7479  acnccim  7491  dfplpq2  7574  recclnq  7612  subhalfnqq  7634  distrnq0  7679  prarloclem3step  7716  genpml  7737  genpmu  7738  addnqprl  7749  addnqpru  7750  appdivnq  7783  mulnqprl  7788  mulnqpru  7789  mullocpr  7791  ltexprlemfl  7829  ltexprlemfu  7831  ltmprr  7862  archpr  7863  cauappcvgprlemm  7865  caucvgprlemladdrl  7898  caucvgprprlemopl  7917  caucvgprprlemopu  7919  recexgt0sr  7993  mulgt0sr  7998  elrealeu  8049  axcaucvglemcau  8118  axcaucvglemres  8119  cnegex  8357  apirr  8785  mulge0  8799  lemul12a  9042  lediv2a  9075  creur  9139  nndiv  9184  zaddcllemneg  9518  peano5uzti  9588  supinfneg  9829  infsupneg  9830  divfnzn  9855  xrltso  10031  xpncan  10106  xltadd1  10111  xleaddadd  10122  elioc2  10171  elico2  10172  elicc2  10173  exfzdc  10487  zsupcllemstep  10490  infssuzex  10494  suprzubdc  10497  exbtwnzlemex  10510  rebtwn2z  10515  modqid  10612  modqcyc  10622  mulqaddmodid  10627  modqadd2mod  10637  addmodlteq  10661  frecuzrdgg  10679  nninfinf  10706  seq3val  10723  seqvalcd  10724  seq3clss  10734  iseqf1olemqcl  10762  iseqf1olemnab  10764  seq3f1olemp  10778  seq3f1o  10780  seqf1oglem1  10782  seqfeq4g  10794  fser0const  10798  ser3ge0  10799  exp3vallem  10803  qsqeqor  10913  facndiv  11002  faclbnd  11004  bcval5  11026  hashen  11047  fihashdom  11067  hashunlem  11068  hashfacen  11101  zfz1isolemiso  11104  seq3coll  11107  ccatsymb  11183  ccatrn  11190  ccatw2s1p2  11227  swrdccatin1  11310  swrdccatin2  11314  swrdccat3b  11325  caucvgre  11559  resqrexlemlo  11591  cau3lem  11692  qdenre  11780  rexico  11799  fimaxre2  11805  2zinfmin  11821  xrmaxiflemcl  11823  xrmaxifle  11824  xrmaxiflemcom  11827  2clim  11879  cn1lem  11892  climsqz  11913  climsqz2  11914  climcau  11925  sumrbdclem  11956  summodclem2a  11960  fsum3  11966  fsumcl2lem  11977  fsumadd  11985  sumsnf  11988  fsum2dlemstep  12013  fisum0diag2  12026  fsummulc2  12027  mertenslemub  12113  mertenslemi1  12114  mertensabs  12116  ntrivcvgap  12127  prodrbdclem  12150  prodmodclem3  12154  prodmodclem2a  12155  prodmodc  12157  prod1dc  12165  prodsnf  12171  fprod2dlemstep  12201  efaddlem  12253  tanaddaplem  12317  zdvdsdc  12391  dvdseq  12427  dvdsext  12434  odd2np1  12452  sqoddm1div8z  12465  nno  12485  dfgcd3  12599  nninfctlemfo  12629  dvdslcm  12659  lcmneg  12664  lcmgcdlem  12667  ncoprmgcdne1b  12679  qredeq  12686  qredeu  12687  divgcdcoprm0  12691  exprmfct  12728  prmdvdsfz  12729  isprm5  12732  rpexp1i  12744  sqrt2irr  12752  nonsq  12797  eulerthlemrprm  12819  eulerthlema  12820  phisum  12831  modprmn0modprm0  12847  pclemdc  12879  pcz  12923  pcmpt  12934  fldivp1  12939  pcfac  12941  expnprm  12944  oddprmdvds  12945  prmpwdvds  12946  infpnlem1  12950  1arith  12958  4sqlem2  12980  4sqlemafi  12986  4sqleminfi  12988  4sqexercise2  12990  4sqlemsdc  12991  ctinfom  13067  enctlem  13071  nninfdclemlt  13090  setsfun  13135  setsfun0  13136  setscom  13140  gsumfzval  13492  mndissubm  13576  resmhm  13588  resmhm2  13589  mhmco  13591  gsumfzz  13596  gsumwsubmcl  13597  gsumwmhm  13599  dfgrp2  13628  isgrpinv  13655  mulgval  13727  mulgnnp1  13735  mulgz  13755  grpissubg  13799  resghm  13865  qusecsub  13936  isrng  13966  lmodfopne  14359  dflidl2rng  14514  gsumfzfsumlemm  14620  mulgrhm2  14643  znidomb  14691  znunit  14692  psrbaglesuppg  14705  psrbagfi  14706  tgdom  14815  ssrest  14925  cnfval  14937  cnpfval  14938  cnpval  14941  iscnp3  14946  ssidcn  14953  cnpnei  14962  cnntr  14968  cncnp  14973  cnptopresti  14981  tx1cn  15012  upxp  15015  imasnopn  15042  bdmet  15245  metcnp  15255  ivthinclemlr  15380  ivthinclemur  15382  ivthinc  15386  dvrecap  15456  dvmptfsum  15468  elply2  15478  plymullem1  15491  plycolemc  15501  plycjlemc  15503  dvply1  15508  pilem3  15526  relogeftb  15608  logbgcd1irr  15710  mpodvdsmulf1o  15733  mersenne  15740  lgslem4  15751  lgsval  15752  lgsfvalg  15753  lgsval2lem  15758  lgsmod  15774  lgsdir2lem4  15779  lgsdinn0  15796  lgsquad2lem2  15830  lgsquad3  15832  2lgslem1c  15838  2sqlem6  15868  2sqlem7  15869  isupgren  15965  wrdupgren  15966  isumgren  15975  wrdumgren  15976  isuspgren  16027  isusgren  16028  clwwlkext2edg  16292  clwwlknonex2  16309  depindlem3  16378  2omap  16645  pw1map  16647  nnsf  16658  peano4nninf  16659  nninfalllem1  16661  nninfsellemqall  16668  nninfsellemeqinf  16669  nninffeq  16673  exmidsbthrlem  16677  isomninnlem  16685  iswomninnlem  16705  iswomni0  16707  ismkvnnlem  16708