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  4563  en2lp  4591  foun  5526  f1oprg  5551  fcof1o  5839  foeqcnvco  5840  f1eqcocnv  5841  caovord3  6101  f1o2ndf1  6295  smores2  6361  frecrdg  6475  nnaordex  6595  xpdom2  6899  xpen  6915  mapen  6916  xpmapenlem  6919  nndomo  6934  phpm  6935  fidifsnen  6940  isinfinf  6967  finexdc  6972  fientri3  6985  fiintim  7001  xpfi  7002  f1dmvrnfibi  7019  sbthlemi8  7039  djudom  7168  omp1eomlem  7169  difinfsn  7175  ctmlemr  7183  ctssdccl  7186  nnnninfeq  7203  enomnilem  7213  finomni  7215  ismkvnex  7230  enmkvlem  7236  nninfwlpoimlemginf  7251  exmidfodomrlemrALT  7282  exmidontriim  7308  netap  7337  exmidapne  7343  acnccim  7355  dfplpq2  7438  recclnq  7476  subhalfnqq  7498  distrnq0  7543  prarloclem3step  7580  genpml  7601  genpmu  7602  addnqprl  7613  addnqpru  7614  appdivnq  7647  mulnqprl  7652  mulnqpru  7653  mullocpr  7655  ltexprlemfl  7693  ltexprlemfu  7695  ltmprr  7726  archpr  7727  cauappcvgprlemm  7729  caucvgprlemladdrl  7762  caucvgprprlemopl  7781  caucvgprprlemopu  7783  recexgt0sr  7857  mulgt0sr  7862  elrealeu  7913  axcaucvglemcau  7982  axcaucvglemres  7983  cnegex  8221  apirr  8649  mulge0  8663  lemul12a  8906  lediv2a  8939  creur  9003  nndiv  9048  zaddcllemneg  9382  peano5uzti  9451  supinfneg  9686  infsupneg  9687  divfnzn  9712  xrltso  9888  xpncan  9963  xltadd1  9968  xleaddadd  9979  elioc2  10028  elico2  10029  elicc2  10030  exfzdc  10333  zsupcllemstep  10336  infssuzex  10340  suprzubdc  10343  exbtwnzlemex  10356  rebtwn2z  10361  modqid  10458  modqcyc  10468  mulqaddmodid  10473  modqadd2mod  10483  addmodlteq  10507  frecuzrdgg  10525  nninfinf  10552  seq3val  10569  seqvalcd  10570  seq3clss  10580  iseqf1olemqcl  10608  iseqf1olemnab  10610  seq3f1olemp  10624  seq3f1o  10626  seqf1oglem1  10628  seqfeq4g  10640  fser0const  10644  ser3ge0  10645  exp3vallem  10649  qsqeqor  10759  facndiv  10848  faclbnd  10850  bcval5  10872  hashen  10893  fihashdom  10912  hashunlem  10913  hashfacen  10945  zfz1isolemiso  10948  seq3coll  10951  caucvgre  11163  resqrexlemlo  11195  cau3lem  11296  qdenre  11384  rexico  11403  fimaxre2  11409  2zinfmin  11425  xrmaxiflemcl  11427  xrmaxifle  11428  xrmaxiflemcom  11431  2clim  11483  cn1lem  11496  climsqz  11517  climsqz2  11518  climcau  11529  sumrbdclem  11559  summodclem2a  11563  fsum3  11569  fsumcl2lem  11580  fsumadd  11588  sumsnf  11591  fsum2dlemstep  11616  fisum0diag2  11629  fsummulc2  11630  mertenslemub  11716  mertenslemi1  11717  mertensabs  11719  ntrivcvgap  11730  prodrbdclem  11753  prodmodclem3  11757  prodmodclem2a  11758  prodmodc  11760  prod1dc  11768  prodsnf  11774  fprod2dlemstep  11804  efaddlem  11856  tanaddaplem  11920  zdvdsdc  11994  dvdseq  12030  dvdsext  12037  odd2np1  12055  sqoddm1div8z  12068  nno  12088  dfgcd3  12202  nninfctlemfo  12232  dvdslcm  12262  lcmneg  12267  lcmgcdlem  12270  ncoprmgcdne1b  12282  qredeq  12289  qredeu  12290  divgcdcoprm0  12294  exprmfct  12331  prmdvdsfz  12332  isprm5  12335  rpexp1i  12347  sqrt2irr  12355  nonsq  12400  eulerthlemrprm  12422  eulerthlema  12423  phisum  12434  modprmn0modprm0  12450  pclemdc  12482  pcz  12526  pcmpt  12537  fldivp1  12542  pcfac  12544  expnprm  12547  oddprmdvds  12548  prmpwdvds  12549  infpnlem1  12553  1arith  12561  4sqlem2  12583  4sqlemafi  12589  4sqleminfi  12591  4sqexercise2  12593  4sqlemsdc  12594  ctinfom  12670  enctlem  12674  nninfdclemlt  12693  setsfun  12738  setsfun0  12739  setscom  12743  gsumfzval  13093  mndissubm  13177  resmhm  13189  resmhm2  13190  mhmco  13192  gsumfzz  13197  gsumwsubmcl  13198  gsumwmhm  13200  dfgrp2  13229  isgrpinv  13256  mulgval  13328  mulgnnp1  13336  mulgz  13356  grpissubg  13400  resghm  13466  qusecsub  13537  isrng  13566  lmodfopne  13958  dflidl2rng  14113  gsumfzfsumlemm  14219  mulgrhm2  14242  znidomb  14290  znunit  14291  psrbaglesuppg  14302  tgdom  14392  ssrest  14502  cnfval  14514  cnpfval  14515  cnpval  14518  iscnp3  14523  ssidcn  14530  cnpnei  14539  cnntr  14545  cncnp  14550  cnptopresti  14558  tx1cn  14589  upxp  14592  imasnopn  14619  bdmet  14822  metcnp  14832  ivthinclemlr  14957  ivthinclemur  14959  ivthinc  14963  dvrecap  15033  dvmptfsum  15045  elply2  15055  plymullem1  15068  plycolemc  15078  plycjlemc  15080  dvply1  15085  pilem3  15103  relogeftb  15185  logbgcd1irr  15287  mpodvdsmulf1o  15310  mersenne  15317  lgslem4  15328  lgsval  15329  lgsfvalg  15330  lgsval2lem  15335  lgsmod  15351  lgsdir2lem4  15356  lgsdinn0  15373  lgsquad2lem2  15407  lgsquad3  15409  2lgslem1c  15415  2sqlem6  15445  2sqlem7  15446  2omap  15726  nnsf  15736  peano4nninf  15737  nninfalllem1  15739  nninfsellemqall  15746  nninfsellemeqinf  15747  nninffeq  15751  exmidsbthrlem  15753  isomninnlem  15761  iswomninnlem  15780  iswomni0  15782  ismkvnnlem  15783