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  621  mt2d  626  mpjaod  719  stdcndcOLD  847  impidc  859  jadc  864  pm2.54dc  892  oplem1  977  mp3and  1351  xor3dc  1398  exlimdd  1886  exlimddv  1913  eqrdav  2195  necon1aidc  2418  necon1bidc  2419  necon4aidc  2435  reximddv  2600  reximssdv  2601  rexlimddv  2619  vtoclgft  2814  rspcedvd  2874  sseldd  3185  ssneldd  3187  tpid3g  3738  preq12b  3801  axpweq  4205  exmid1dc  4234  exmid1stab  4242  opth  4271  issod  4355  frirrg  4386  frind  4388  ralxfr2d  4500  rexxfr2d  4501  eldifpw  4513  onun2  4527  onuni  4531  elirr  4578  en2lp  4591  wetriext  4614  peano2  4632  relop  4817  elres  4983  sotri2  5068  iota4an  5240  iota5  5241  funeu  5284  funopg  5293  imadiflem  5338  funimaexglem  5342  ssimaex  5625  ffvelcdm  5698  dff3im  5710  dffo4  5713  f1eqcocnv  5841  f1oiso2  5877  riota5f  5905  riotass2  5907  acexmidlemcase  5920  ovmpodf  6058  ovmpodv2  6060  ovi3  6064  ov6g  6065  caoftrn  6172  op1steq  6246  tfr0dm  6389  tfrlemibxssdm  6394  tfrlemi14d  6400  tfr1onlembxssdm  6410  tfr1onlemaccex  6415  tfr1onlemres  6416  tfrcllembxssdm  6423  tfrcllemaccex  6428  tfrcllemres  6429  rdgivallem  6448  nnsucelsuc  6558  nnsucsssuc  6559  dcdifsnid  6571  nnawordex  6596  ersym  6613  mapvalg  6726  pmvalg  6727  mapsn  6758  fundmen  6874  pw2f1odclem  6904  mapdom1g  6917  fidceq  6939  fin0or  6956  findcard2  6959  findcard2s  6960  prfidceq  6998  fiintim  7001  suplub2ti  7076  supsnti  7080  supisoex  7084  difinfsnlem  7174  difinfsn  7175  ctm  7184  ctssdclemn0  7185  ctssdccl  7186  ctssdc  7188  enumctlemm  7189  nninfninc  7198  nnnninfeq2  7204  enomnilem  7213  exmidomniim  7216  exmidomni  7217  fodjuomnilemdc  7219  fodjuomnilemres  7223  omnimkv  7231  mkvprop  7233  omniwomnimkv  7242  en2eleq  7276  acfun  7292  exmidontriimlem1  7306  exmidontriimlem4  7309  exmidontriim  7310  ccfunen  7349  cc4f  7354  cc4n  7356  elni2  7400  mulclpi  7414  nlt1pig  7427  indpi  7428  recclnq  7478  ltexnqq  7494  halfnqq  7496  prarloclemarch  7504  prarloclemarch2  7505  prop  7561  prltlu  7573  prarloclem3step  7582  prarloclem5  7586  prarloclem  7587  prarloc  7589  prarloc2  7590  genpml  7603  genpmu  7604  genprndl  7607  genprndu  7608  genpdisj  7609  addnqprllem  7613  addnqprulem  7614  addlocprlemeq  7619  addlocprlemgt  7620  addlocprlem  7621  addlocpr  7622  nqprloc  7631  nqprl  7637  nqpru  7638  addnqprlemrl  7643  addnqprlemru  7644  appdivnq  7649  prmuloc  7652  prmuloc2  7653  mullocprlem  7656  mullocpr  7657  mulnqprlemrl  7659  mulnqprlemru  7660  ltprordil  7675  ltpopr  7681  ltsopr  7682  ltaddpr  7683  ltexprlemm  7686  ltexprlemopl  7687  ltexprlemlol  7688  ltexprlemopu  7689  ltexprlemupu  7690  ltexprlemloc  7693  ltexprlemfl  7695  ltexprlemrl  7696  ltexprlemfu  7697  ltexprlemru  7698  ltaprg  7705  recexprlemm  7710  recexprlem1ssl  7719  recexprlem1ssu  7720  aptiprleml  7725  aptiprlemu  7726  archpr  7729  cauappcvgprlemm  7731  cauappcvgprlemopl  7732  cauappcvgprlemlol  7733  cauappcvgprlemopu  7734  cauappcvgprlemupu  7735  cauappcvgprlemdisj  7737  cauappcvgprlemloc  7738  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  cauappcvgprlemladdru  7742  cauappcvgprlem1  7745  archrecpr  7750  caucvgprlemnkj  7752  caucvgprlemnbj  7753  caucvgprlemm  7754  caucvgprlemopl  7755  caucvgprlemlol  7756  caucvgprlemopu  7757  caucvgprlemupu  7758  caucvgprlemdisj  7760  caucvgprlemloc  7761  caucvgprlemladdfu  7763  caucvgprlem1  7765  caucvgprlemlim  7767  caucvgprprlemnbj  7779  caucvgprprlemml  7780  caucvgprprlemopl  7783  caucvgprprlemlol  7784  caucvgprprlemopu  7785  caucvgprprlemupu  7786  caucvgprprlemdisj  7788  caucvgprprlemloc  7789  caucvgprprlemexbt  7792  caucvgprprlemaddq  7794  caucvgprprlemlim  7797  suplocexprlemss  7801  suplocexprlemrl  7803  suplocexprlemmu  7804  suplocexprlemru  7805  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemub  7809  suplocexprlemlub  7810  recexgt0sr  7859  mulgt0sr  7864  archsr  7868  caucvgsrlemoffcau  7884  suplocsrlemb  7892  suplocsrlempr  7893  suplocsrlem  7894  cnm  7918  axarch  7977  axcaucvglemcau  7984  axpre-suploclemres  7987  lelttr  8134  ltletr  8135  ltled  8164  cnegexlem1  8220  cnegexlem2  8221  renegcl  8306  negf1o  8427  gt0add  8619  apreap  8633  apirr  8651  apsym  8652  apcotr  8653  apadd1  8654  apneg  8657  mulext1  8658  mulap0r  8661  apti  8668  aprcl  8692  aptap  8696  recexap  8699  mulap0  8700  receuap  8715  mul0eqap  8716  lep1  8891  lem1  8893  letrp1  8894  recreclt  8946  lbinf  8994  suprubex  8997  nnrecgt0  9047  bndndx  9267  nn0ge2m1nn  9328  elnn0z  9358  peano2z  9381  zaddcl  9385  ztri3or0  9387  zltnle  9391  zdceq  9420  zdcle  9421  zdclt  9422  zdiv  9433  zeo  9450  fnn0ind  9461  btwnz  9464  uzm1  9651  uzp1  9654  indstr  9686  supinfneg  9688  infsupneg  9689  eluzdc  9703  nn01to3  9710  qapne  9732  xrltled  9893  xrlelttr  9900  xrltletr  9901  ge0nemnf  9918  fzdcel  10134  elfzouz2  10256  fzoss1  10266  fzospliti  10271  fzocatel  10294  fzostep1  10332  zsupcllemstep  10338  zsupcl  10340  infssuzledc  10343  qtri3or  10349  qltnle  10352  qdceq  10353  qdclt  10354  exbtwnzlemex  10358  rebtwn2zlemstep  10361  rebtwn2z  10363  qbtwnxr  10366  ioom  10369  ico0  10370  ioc0  10371  flqeqceilz  10429  modqadd1  10472  modqmul1  10488  frec2uzuzd  10513  frec2uzlt2d  10515  frec2uzf1od  10517  frecuzrdgrrn  10519  frec2uzrdg  10520  frecuzrdgrcl  10521  frecuzrdgsuc  10525  frecuzrdgrclt  10526  frecuzrdgdomlem  10528  uzsinds  10555  seqvalcd  10572  seqovcd  10578  seq3fveq2  10586  seqfveq2g  10588  seq3shft2  10592  seqshft2g  10593  monoord  10596  seq3split  10599  seqsplitg  10600  seq3caopr3  10602  iseqf1olemab  10613  iseqf1olemnanb  10614  iseqf1olemqk  10618  seqf1oglem1  10630  seqf1og  10632  seq3id3  10635  seq3id2  10637  seq3homo  10638  seqhomog  10641  expgt1  10688  m1expeven  10697  expnbnd  10774  expnlbnd2  10776  nn0ltexp2  10820  apexp1  10829  hashennn  10891  zfz1isolem1  10951  seq3coll  10953  cjap  11090  caucvgre  11165  cvg1nlemres  11169  resqrexlemgt0  11204  resqrexlemglsq  11206  resqrexlemga  11207  resqrtcl  11213  abslt  11272  abssubap0  11274  abssubne0  11275  caubnd2  11301  qdenre  11386  maxabslemlub  11391  maxabs  11393  maxleast  11397  fimaxre2  11411  xrmaxiflemlub  11432  xrmaxif  11435  xrmaxltsup  11442  xrmaxadd  11445  xrmineqinf  11453  climuni  11477  2clim  11485  climcn1  11492  climcn2  11493  subcn2  11495  mulcn2  11496  climsqz  11519  climsqz2  11520  climcau  11531  climcvg1nlem  11533  climcaucn  11535  serf0  11536  sumrbdclem  11561  summodclem2  11566  zsumdc  11568  divcnv  11681  absltap  11693  absgtap  11694  mertenslem2  11720  ntrivcvgap  11732  prodrbdclem  11755  prodmodclem2  11761  zproddc  11763  prodssdc  11773  fprodsplitdc  11780  fprodcl2lem  11789  efcllemp  11842  tanvalap  11892  sin01bnd  11941  cos01bnd  11942  sin01gt0  11946  absef  11954  eirrap  11962  dvds0  11990  dvdsmul1  11997  dvdsmultr1d  12016  dvdslelemd  12027  divconjdvds  12033  alzdvds  12038  3dvds  12048  sqoddm1div8z  12070  nno  12090  divalglemex  12106  bits0o  12134  dvdsbnd  12150  dvdslegcd  12158  zeqzmulgcd  12164  gcd0id  12173  gcdaddm  12178  gcd1  12181  gcdabs  12182  bezoutlemnewy  12190  bezoutlemstep  12191  bezoutlemmain  12192  bezoutlemex  12195  bezoutlemzz  12196  bezoutlemaz  12197  bezoutlembz  12198  bezoutlembi  12199  bezoutlemle  12202  bezoutlemsup  12203  mulgcd  12210  gcdzeq  12216  dvdsmulgcd  12219  sqgcd  12223  bezoutr1  12227  nninfctlemfo  12234  algcvga  12246  algfx  12247  eucalglt  12252  eucalg  12254  lcmneg  12269  lcmabs  12271  lcmgcdlem  12272  ncoprmgcdne1b  12284  mulgcddvds  12289  qredeq  12291  divgcdcoprm0  12296  cncongr1  12298  isprm2lem  12311  nprm  12318  dvdsnprmd  12320  prmdvdsfz  12334  isprm5lem  12336  coprm  12339  isprm6  12342  sqrt2irr  12357  pw2dvdslemn  12360  pw2dvdseulemle  12362  oddpwdclemdvds  12365  oddpwdclemndvds  12366  sqrt2irrap  12375  qnumdencl  12382  prmdiv  12430  modprmn0modprm0  12452  prm23lt5  12459  pythagtriplem4  12464  pythagtriplem19  12478  pythagtrip  12479  pclemub  12483  pcpre1  12488  pcpremul  12489  pceulem  12490  pcqcl  12502  pcidlem  12519  pcgcd1  12524  pc2dvds  12526  dvdsprmpweqle  12533  difsqpwdvds  12534  pcadd  12536  pcmpt  12539  expnprm  12549  pockthg  12553  infpnlem2  12556  prmunb  12558  1arith  12563  4sqlem10  12583  4sqlem11  12597  4sqlem12  12598  4sqlem13m  12599  4sqlem17  12603  4sqlem18  12604  ennnfonelemex  12658  ennnfonelemhom  12659  ennnfonelemrnh  12660  ennnfonelemnn0  12666  ennnfonelemim  12668  exmidunben  12670  ctinfomlemom  12671  ctinfom  12672  ctinf  12674  omctfn  12687  nninfdclemp1  12694  setscomd  12746  imasaddfnlemg  13018  mhmf1o  13174  grpinveu  13242  grpasscan1  13267  dfgrp3mlem  13302  grp1inv  13311  issubg4m  13401  ghmf1o  13483  srgisid  13620  ringadd2  13661  ringinvnzdiv  13684  unitgrp  13750  ringelnzr  13821  lringuplu  13830  subrguss  13870  subrgintm  13877  aprcotr  13919  islmodd  13927  lssclg  13998  lss0cl  14003  lssvneln0  14007  lss1d  14017  lmodindp1  14062  rnglidlmmgm  14130  znidomb  14292  znunit  14293  znrrg  14294  mplsubgfilemcl  14333  mplsubgfileminv  14334  tgcl  14408  neii1  14491  neii2  14493  neiss  14494  tpnei  14504  tgrest  14513  ssrest  14526  icnpimaex  14555  lmcvg  14561  cnpnei  14563  cnptopco  14566  lmff  14593  txcnp  14615  txcn  14619  hmeontr  14657  blssec  14782  mopni3  14828  blsscls2  14837  comet  14843  bdxmet  14845  bdmopn  14848  xmettxlem  14853  xmettx  14854  addcncntoplem  14905  mpomulcn  14910  mulc1cncf  14933  cncfco  14935  cncfmptc  14940  mulcncflem  14951  mulcncf  14952  dedekindeulemlu  14965  dedekindeulemeu  14966  suplociccreex  14968  suplociccex  14969  dedekindicclemlu  14974  dedekindicclemeu  14975  ivthinclemlopn  14980  ivthinclemlr  14981  ivthinclemuopn  14982  ivthinclemur  14983  ivthinclemloc  14985  ivthinc  14987  ivthreinc  14989  ivthdichlem  14995  limcimolemlt  15008  limcresi  15010  cnplimcim  15011  cnplimclemle  15012  cnplimclemr  15013  limccnpcntop  15019  limccoap  15022  dvcoapbr  15051  dvcj  15053  plyf  15081  plyaddlem1  15091  plymullem1  15092  plyco  15103  plycj  15105  plycn  15106  plyrecj  15107  dvply2g  15110  efltlemlt  15118  sin0pilem2  15126  tangtx  15182  logdivlti  15225  rplogbval  15289  logbgcd1irraplemexp  15312  logbgcd1irraplemap  15313  logbgcd1irrap  15314  perfect1  15342  perfectlem1  15343  perfectlem2  15344  lgsval4a  15371  lgsdir2lem3  15379  lgsne0  15387  gausslemma2dlem3  15412  gausslemma2dlem4  15413  gausslemma2dlem6  15416  gausslemma2dlem7  15417  gausslemma2d  15418  lgseisenlem1  15419  lgsquadlem2  15427  lgsquadlem3  15428  lgsquad2lem2  15431  lgsquad3  15433  2lgsoddprmlem2  15455  2sqlem8a  15471  2sqlem8  15472  2sqlem9  15473  bj-exlimmpi  15524  uzdcinzz  15552  bj-charfundcALT  15563  bj-2inf  15692  bj-peano4  15709  bj-nn0suc  15718  1dom1el  15745  subctctexmid  15755  nninfalllem1  15763  nninfsellemqall  15770  nninfomnilem  15773  nninffeq  15775  nnnninfex  15777  exmidsbthrlem  15779  sbthomlem  15782  refeq  15785  isomninnlem  15787  apdifflemr  15804  redcwlpo  15812  reap0  15815  nconstwlpolem  15822