Theorem mpd 13

Description: A modus ponens deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
mpd.1	|- ( ph -> ps )
mpd.2	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
mpd	|- ( ph -> ch )

Proof of Theorem mpd

Step	Hyp	Ref	Expression
1		mpd.1	. 2 |- ( ph -> ps )
2		mpd.2	. . 3 |- ( ph -> ( ps -> ch ) )
3	2	a2i 11	. 2 |- ( ( ph -> ps ) -> ( ph -> ch ) )
4	1, 3	ax-mp 5	1 |- ( ph -> ch )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-2 7

This theorem is referenced by:  syl  14  mpi  15  id  19  mpcom  36  mpdd  41  mp2d  47  pm2.43i  49  syl3c  63  mpbid  147  mpbird  167  jcai  311  mp2and  433  pm2.21dd  625  mt2d  630  mpnanrd  700  mpjaod  726  stdcndcOLD  854  impidc  866  jadc  871  pm2.54dc  899  oplem1  984  mp3and  1377  xor3dc  1432  exlimdd  1920  exlimddv  1947  eqrdav  2230  necon1aidc  2454  necon1bidc  2455  necon4aidc  2471  reximddv  2636  reximssdv  2637  rexlimddv  2656  vtoclgft  2855  rspcedvd  2917  sseldd  3229  ssneldd  3231  tpid3g  3791  preq12b  3858  axpweq  4267  exmid1dc  4296  exmid1stab  4304  opth  4335  issod  4422  frirrg  4453  frind  4455  ralxfr2d  4567  rexxfr2d  4568  eldifpw  4580  onun2  4594  onuni  4598  elirr  4645  en2lp  4658  wetriext  4681  peano2  4699  relop  4886  elres  5055  sotri2  5141  iota4an  5314  iota5  5315  funeu  5358  funopg  5367  imadiflem  5416  funimaexglem  5420  ssimaex  5716  ffvelcdm  5788  dff3im  5800  dffo4  5803  funopsn  5838  f1eqcocnv  5942  f1oiso2  5978  riota5f  6008  riotass2  6010  acexmidlemcase  6023  elovimad  6072  ovmpodf  6163  ovmpodv2  6165  ovi3  6169  ov6g  6170  caoftrn  6277  op1steq  6351  fvdifsuppst  6422  suppssdc  6438  suppofss1dcl  6442  suppofss2dcl  6443  tfr0dm  6531  tfrlemibxssdm  6536  tfrlemi14d  6542  tfr1onlembxssdm  6552  tfr1onlemaccex  6557  tfr1onlemres  6558  tfrcllembxssdm  6565  tfrcllemaccex  6570  tfrcllemres  6571  rdgivallem  6590  nnsucelsuc  6702  nnsucsssuc  6703  dcdifsnid  6715  nnawordex  6740  ersym  6757  mapvalg  6870  pmvalg  6871  mapsn  6902  fundmen  7024  1dom1el  7036  en2  7041  pw2f1odclem  7063  mapdom1g  7076  fidceq  7099  fin0or  7118  findcard2  7121  findcard2s  7122  fidcen  7131  prfidceq  7163  fiintim  7166  suplub2ti  7243  supsnti  7247  supisoex  7251  difinfsnlem  7341  difinfsn  7342  ctm  7351  ctssdclemn0  7352  ctssdccl  7353  ctssdc  7355  enumctlemm  7356  nninfninc  7365  nnnninfeq2  7371  enomnilem  7380  exmidomniim  7383  exmidomni  7384  fodjuomnilemdc  7386  fodjuomnilemres  7390  omnimkv  7398  mkvprop  7400  omniwomnimkv  7409  en2prde  7441  pr2cv1  7443  en2eleq  7449  acfun  7465  exmidontriimlem1  7479  exmidontriimlem4  7482  exmidontriim  7483  ccfunen  7526  cc4f  7531  cc4n  7533  elni2  7577  mulclpi  7591  nlt1pig  7604  indpi  7605  recclnq  7655  ltexnqq  7671  halfnqq  7673  prarloclemarch  7681  prarloclemarch2  7682  prop  7738  prltlu  7750  prarloclem3step  7759  prarloclem5  7763  prarloclem  7764  prarloc  7766  prarloc2  7767  genpml  7780  genpmu  7781  genprndl  7784  genprndu  7785  genpdisj  7786  addnqprllem  7790  addnqprulem  7791  addlocprlemeq  7796  addlocprlemgt  7797  addlocprlem  7798  addlocpr  7799  nqprloc  7808  nqprl  7814  nqpru  7815  addnqprlemrl  7820  addnqprlemru  7821  appdivnq  7826  prmuloc  7829  prmuloc2  7830  mullocprlem  7833  mullocpr  7834  mulnqprlemrl  7836  mulnqprlemru  7837  ltprordil  7852  ltpopr  7858  ltsopr  7859  ltaddpr  7860  ltexprlemm  7863  ltexprlemopl  7864  ltexprlemlol  7865  ltexprlemopu  7866  ltexprlemupu  7867  ltexprlemloc  7870  ltexprlemfl  7872  ltexprlemrl  7873  ltexprlemfu  7874  ltexprlemru  7875  ltaprg  7882  recexprlemm  7887  recexprlem1ssl  7896  recexprlem1ssu  7897  aptiprleml  7902  aptiprlemu  7903  archpr  7906  cauappcvgprlemm  7908  cauappcvgprlemopl  7909  cauappcvgprlemlol  7910  cauappcvgprlemopu  7911  cauappcvgprlemupu  7912  cauappcvgprlemdisj  7914  cauappcvgprlemloc  7915  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  cauappcvgprlemladdru  7919  cauappcvgprlem1  7922  archrecpr  7927  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemm  7931  caucvgprlemopl  7932  caucvgprlemlol  7933  caucvgprlemopu  7934  caucvgprlemupu  7935  caucvgprlemdisj  7937  caucvgprlemloc  7938  caucvgprlemladdfu  7940  caucvgprlem1  7942  caucvgprlemlim  7944  caucvgprprlemnbj  7956  caucvgprprlemml  7957  caucvgprprlemopl  7960  caucvgprprlemlol  7961  caucvgprprlemopu  7962  caucvgprprlemupu  7963  caucvgprprlemdisj  7965  caucvgprprlemloc  7966  caucvgprprlemexbt  7969  caucvgprprlemaddq  7971  caucvgprprlemlim  7974  suplocexprlemss  7978  suplocexprlemrl  7980  suplocexprlemmu  7981  suplocexprlemru  7982  suplocexprlemdisj  7983  suplocexprlemloc  7984  suplocexprlemub  7986  suplocexprlemlub  7987  recexgt0sr  8036  mulgt0sr  8041  archsr  8045  caucvgsrlemoffcau  8061  suplocsrlemb  8069  suplocsrlempr  8070  suplocsrlem  8071  cnm  8095  axarch  8154  axcaucvglemcau  8161  axpre-suploclemres  8164  lelttr  8310  ltletr  8311  ltled  8340  cnegexlem1  8396  cnegexlem2  8397  renegcl  8482  negf1o  8603  gt0add  8795  apreap  8809  apirr  8827  apsym  8828  apcotr  8829  apadd1  8830  apneg  8833  mulext1  8834  mulap0r  8837  apti  8844  aprcl  8868  aptap  8872  recexap  8875  mulap0  8876  receuap  8891  mul0eqap  8892  lep1  9067  lem1  9069  letrp1  9070  recreclt  9122  lbinf  9170  suprubex  9173  nnrecgt0  9223  bndndx  9443  nn0ge2m1nn  9506  elnn0z  9536  peano2z  9559  zaddcl  9563  ztri3or0  9565  zltnle  9569  zdceq  9599  zdcle  9600  zdclt  9601  zdiv  9612  zeo  9629  fnn0ind  9640  btwnz  9643  uzm1  9831  uzp1  9834  indstr  9871  supinfneg  9873  infsupneg  9874  eluzdc  9888  nn01to3  9895  qapne  9917  xrltled  10078  xrlelttr  10085  xrltletr  10086  ge0nemnf  10103  fzdcel  10320  elfzouz2  10442  fzoss1  10453  fzospliti  10458  elincfzoext  10484  fzocatel  10490  fzostep1  10529  zsupcllemstep  10535  zsupcl  10537  infssuzledc  10540  qtri3or  10546  qltnle  10549  qdceq  10550  qdclt  10551  exbtwnzlemex  10555  rebtwn2zlemstep  10558  rebtwn2z  10560  qbtwnxr  10563  ioom  10566  ico0  10567  ioc0  10568  flqeqceilz  10626  modqadd1  10669  modqmul1  10685  frec2uzuzd  10710  frec2uzlt2d  10712  frec2uzf1od  10714  frecuzrdgrrn  10716  frec2uzrdg  10717  frecuzrdgrcl  10718  frecuzrdgsuc  10722  frecuzrdgrclt  10723  frecuzrdgdomlem  10725  uzsinds  10752  seqvalcd  10769  seqovcd  10775  seq3fveq2  10783  seqfveq2g  10785  seq3shft2  10789  seqshft2g  10790  monoord  10793  seq3split  10796  seqsplitg  10797  seq3caopr3  10799  iseqf1olemab  10810  iseqf1olemnanb  10811  iseqf1olemqk  10815  seqf1oglem1  10827  seqf1og  10829  seq3id3  10832  seq3id2  10834  seq3homo  10835  seqhomog  10838  expgt1  10885  m1expeven  10894  expnbnd  10971  expnlbnd2  10973  nn0ltexp2  11017  apexp1  11026  hashennn  11088  zfz1isolem1  11150  seq3coll  11152  pfxwrdsymbg  11320  wrdind  11352  wrd2ind  11353  cjap  11529  caucvgre  11604  cvg1nlemres  11608  resqrexlemgt0  11643  resqrexlemglsq  11645  resqrexlemga  11646  resqrtcl  11652  abslt  11711  abssubap0  11713  abssubne0  11714  caubnd2  11740  qdenre  11825  maxabslemlub  11830  maxabs  11832  maxleast  11836  fimaxre2  11850  xrmaxiflemlub  11871  xrmaxif  11874  xrmaxltsup  11881  xrmaxadd  11884  xrmineqinf  11892  climuni  11916  2clim  11924  climcn1  11931  climcn2  11932  subcn2  11934  mulcn2  11935  climsqz  11958  climsqz2  11959  climcau  11970  climcvg1nlem  11972  climcaucn  11974  serf0  11975  sumrbdclem  12001  summodclem2  12006  zsumdc  12008  divcnv  12121  absltap  12133  absgtap  12134  mertenslem2  12160  ntrivcvgap  12172  prodrbdclem  12195  prodmodclem2  12201  zproddc  12203  prodssdc  12213  fprodsplitdc  12220  fprodcl2lem  12229  efcllemp  12282  tanvalap  12332  sin01bnd  12381  cos01bnd  12382  sin01gt0  12386  absef  12394  eirrap  12402  dvds0  12430  dvdsmul1  12437  dvdsmultr1d  12456  dvdslelemd  12467  divconjdvds  12473  alzdvds  12478  3dvds  12488  sqoddm1div8z  12510  nno  12530  divalglemex  12546  bits0o  12574  dvdsbnd  12590  dvdslegcd  12598  zeqzmulgcd  12604  gcd0id  12613  gcdaddm  12618  gcd1  12621  gcdabs  12622  bezoutlemnewy  12630  bezoutlemstep  12631  bezoutlemmain  12632  bezoutlemex  12635  bezoutlemzz  12636  bezoutlemaz  12637  bezoutlembz  12638  bezoutlembi  12639  bezoutlemle  12642  bezoutlemsup  12643  mulgcd  12650  gcdzeq  12656  dvdsmulgcd  12659  sqgcd  12663  bezoutr1  12667  nninfctlemfo  12674  algcvga  12686  algfx  12687  eucalglt  12692  eucalg  12694  lcmneg  12709  lcmabs  12711  lcmgcdlem  12712  ncoprmgcdne1b  12724  mulgcddvds  12729  qredeq  12731  divgcdcoprm0  12736  cncongr1  12738  isprm2lem  12751  nprm  12758  dvdsnprmd  12760  prmdvdsfz  12774  isprm5lem  12776  coprm  12779  isprm6  12782  sqrt2irr  12797  pw2dvdslemn  12800  pw2dvdseulemle  12802  oddpwdclemdvds  12805  oddpwdclemndvds  12806  sqrt2irrap  12815  qnumdencl  12822  prmdiv  12870  modprmn0modprm0  12892  prm23lt5  12899  pythagtriplem4  12904  pythagtriplem19  12918  pythagtrip  12919  pclemub  12923  pcpre1  12928  pcpremul  12929  pceulem  12930  pcqcl  12942  pcidlem  12959  pcgcd1  12964  pc2dvds  12966  dvdsprmpweqle  12973  difsqpwdvds  12974  pcadd  12976  pcmpt  12979  expnprm  12989  pockthg  12993  infpnlem2  12996  prmunb  12998  1arith  13003  4sqlem10  13023  4sqlem11  13037  4sqlem12  13038  4sqlem13m  13039  4sqlem17  13043  4sqlem18  13044  ennnfonelemex  13098  ennnfonelemhom  13099  ennnfonelemrnh  13100  ennnfonelemnn0  13106  ennnfonelemim  13108  exmidunben  13110  ctinfomlemom  13111  ctinfom  13112  ctinf  13114  omctfn  13127  nninfdclemp1  13134  setscomd  13186  imasaddfnlemg  13460  mhmf1o  13616  grpinveu  13684  grpasscan1  13709  dfgrp3mlem  13744  grp1inv  13753  issubg4m  13843  ghmf1o  13925  srgisid  14063  ringadd2  14104  ringinvnzdiv  14127  unitgrp  14194  ringelnzr  14265  lringuplu  14274  subrguss  14314  subrgintm  14321  aprcotr  14364  islmodd  14372  lssclg  14443  lss0cl  14448  lssvneln0  14452  lss1d  14462  lmodindp1  14507  rnglidlmmgm  14575  znidomb  14737  znunit  14738  znrrg  14739  mplsubgfilemcl  14783  mplsubgfileminv  14784  tgcl  14858  neii1  14941  neii2  14943  neiss  14944  tpnei  14954  tgrest  14963  ssrest  14976  icnpimaex  15005  lmcvg  15011  cnpnei  15013  cnptopco  15016  lmff  15043  txcnp  15065  txcn  15069  hmeontr  15107  blssec  15232  mopni3  15278  blsscls2  15287  comet  15293  bdxmet  15295  bdmopn  15298  xmettxlem  15303  xmettx  15304  addcncntoplem  15355  mpomulcn  15360  mulc1cncf  15383  cncfco  15385  cncfmptc  15390  mulcncflem  15401  mulcncf  15402  dedekindeulemlu  15415  dedekindeulemeu  15416  suplociccreex  15418  suplociccex  15419  dedekindicclemlu  15424  dedekindicclemeu  15425  ivthinclemlopn  15430  ivthinclemlr  15431  ivthinclemuopn  15432  ivthinclemur  15433  ivthinclemloc  15435  ivthinc  15437  ivthreinc  15439  ivthdichlem  15445  limcimolemlt  15458  limcresi  15460  cnplimcim  15461  cnplimclemle  15462  cnplimclemr  15463  limccnpcntop  15469  limccoap  15472  dvcoapbr  15501  dvcj  15503  plyf  15531  plyaddlem1  15541  plymullem1  15542  plyco  15553  plycj  15555  plycn  15556  plyrecj  15557  dvply2g  15560  efltlemlt  15568  sin0pilem2  15576  tangtx  15632  logdivlti  15675  rplogbval  15739  logbgcd1irraplemexp  15762  logbgcd1irraplemap  15763  logbgcd1irrap  15764  perfect1  15795  perfectlem1  15796  perfectlem2  15797  lgsval4a  15824  lgsdir2lem3  15832  lgsne0  15840  gausslemma2dlem3  15865  gausslemma2dlem4  15866  gausslemma2dlem6  15869  gausslemma2dlem7  15870  gausslemma2d  15871  lgseisenlem1  15872  lgsquadlem2  15880  lgsquadlem3  15881  lgsquad2lem2  15884  lgsquad3  15886  2lgsoddprmlem2  15908  2sqlem8a  15924  2sqlem8  15925  2sqlem9  15926  lpvtx  16003  upgrex  16027  upgr1een  16048  edgupgren  16065  umgredg  16069  upgrpredgv  16070  upgredg2vtx  16072  upgredgpr  16073  uspgrf1oedg  16100  usgredg4  16139  uspgredgdomord  16153  usgr1vr  16172  wlkvtxiedg  16269  wlkvtxiedgg  16270  wlk1walkdom  16283  upgriswlkdc  16284  upgrwlkedg  16285  uspgr2wlkeq  16289  uspgr2wlkeqi  16291  umgrwlknloop  16292  eupth2lem2dc  16383  trlsegvdeglem1  16384  eupth2lem3lem4fi  16397  bj-exlimmpi  16471  uzdcinzz  16499  bj-charfundcALT  16508  bj-2inf  16637  bj-peano4  16654  bj-nn0suc  16663  pw1ndom3  16693  subctctexmid  16705  exmidcon  16711  nninfalllem1  16717  nninfsellemqall  16724  nninfomnilem  16727  nninffeq  16729  nnnninfex  16731  exmidsbthrlem  16733  sbthomlem  16736  refeq  16739  isomninnlem  16745  apdifflemr  16762  redcwlpo  16771  reap0  16774  nconstwlpolem  16781