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  720  stdcndcOLD  848  impidc  860  jadc  865  pm2.54dc  893  oplem1  978  mp3and  1353  xor3dc  1407  exlimdd  1896  exlimddv  1923  eqrdav  2205  necon1aidc  2428  necon1bidc  2429  necon4aidc  2445  reximddv  2610  reximssdv  2611  rexlimddv  2629  vtoclgft  2825  rspcedvd  2887  sseldd  3198  ssneldd  3200  tpid3g  3753  preq12b  3817  axpweq  4223  exmid1dc  4252  exmid1stab  4260  opth  4289  issod  4374  frirrg  4405  frind  4407  ralxfr2d  4519  rexxfr2d  4520  eldifpw  4532  onun2  4546  onuni  4550  elirr  4597  en2lp  4610  wetriext  4633  peano2  4651  relop  4836  elres  5004  sotri2  5089  iota4an  5261  iota5  5262  funeu  5305  funopg  5314  imadiflem  5362  funimaexglem  5366  ssimaex  5653  ffvelcdm  5726  dff3im  5738  dffo4  5741  funopsn  5775  f1eqcocnv  5873  f1oiso2  5909  riota5f  5937  riotass2  5939  acexmidlemcase  5952  ovmpodf  6090  ovmpodv2  6092  ovi3  6096  ov6g  6097  caoftrn  6204  op1steq  6278  tfr0dm  6421  tfrlemibxssdm  6426  tfrlemi14d  6432  tfr1onlembxssdm  6442  tfr1onlemaccex  6447  tfr1onlemres  6448  tfrcllembxssdm  6455  tfrcllemaccex  6460  tfrcllemres  6461  rdgivallem  6480  nnsucelsuc  6590  nnsucsssuc  6591  dcdifsnid  6603  nnawordex  6628  ersym  6645  mapvalg  6758  pmvalg  6759  mapsn  6790  fundmen  6912  en2  6926  pw2f1odclem  6946  mapdom1g  6959  fidceq  6981  fin0or  6998  findcard2  7001  findcard2s  7002  prfidceq  7040  fiintim  7043  suplub2ti  7118  supsnti  7122  supisoex  7126  difinfsnlem  7216  difinfsn  7217  ctm  7226  ctssdclemn0  7227  ctssdccl  7228  ctssdc  7230  enumctlemm  7231  nninfninc  7240  nnnninfeq2  7246  enomnilem  7255  exmidomniim  7258  exmidomni  7259  fodjuomnilemdc  7261  fodjuomnilemres  7265  omnimkv  7273  mkvprop  7275  omniwomnimkv  7284  en2eleq  7319  acfun  7335  exmidontriimlem1  7349  exmidontriimlem4  7352  exmidontriim  7353  ccfunen  7396  cc4f  7401  cc4n  7403  elni2  7447  mulclpi  7461  nlt1pig  7474  indpi  7475  recclnq  7525  ltexnqq  7541  halfnqq  7543  prarloclemarch  7551  prarloclemarch2  7552  prop  7608  prltlu  7620  prarloclem3step  7629  prarloclem5  7633  prarloclem  7634  prarloc  7636  prarloc2  7637  genpml  7650  genpmu  7651  genprndl  7654  genprndu  7655  genpdisj  7656  addnqprllem  7660  addnqprulem  7661  addlocprlemeq  7666  addlocprlemgt  7667  addlocprlem  7668  addlocpr  7669  nqprloc  7678  nqprl  7684  nqpru  7685  addnqprlemrl  7690  addnqprlemru  7691  appdivnq  7696  prmuloc  7699  prmuloc2  7700  mullocprlem  7703  mullocpr  7704  mulnqprlemrl  7706  mulnqprlemru  7707  ltprordil  7722  ltpopr  7728  ltsopr  7729  ltaddpr  7730  ltexprlemm  7733  ltexprlemopl  7734  ltexprlemlol  7735  ltexprlemopu  7736  ltexprlemupu  7737  ltexprlemloc  7740  ltexprlemfl  7742  ltexprlemrl  7743  ltexprlemfu  7744  ltexprlemru  7745  ltaprg  7752  recexprlemm  7757  recexprlem1ssl  7766  recexprlem1ssu  7767  aptiprleml  7772  aptiprlemu  7773  archpr  7776  cauappcvgprlemm  7778  cauappcvgprlemopl  7779  cauappcvgprlemlol  7780  cauappcvgprlemopu  7781  cauappcvgprlemupu  7782  cauappcvgprlemdisj  7784  cauappcvgprlemloc  7785  cauappcvgprlemladdfu  7787  cauappcvgprlemladdfl  7788  cauappcvgprlemladdru  7789  cauappcvgprlem1  7792  archrecpr  7797  caucvgprlemnkj  7799  caucvgprlemnbj  7800  caucvgprlemm  7801  caucvgprlemopl  7802  caucvgprlemlol  7803  caucvgprlemopu  7804  caucvgprlemupu  7805  caucvgprlemdisj  7807  caucvgprlemloc  7808  caucvgprlemladdfu  7810  caucvgprlem1  7812  caucvgprlemlim  7814  caucvgprprlemnbj  7826  caucvgprprlemml  7827  caucvgprprlemopl  7830  caucvgprprlemlol  7831  caucvgprprlemopu  7832  caucvgprprlemupu  7833  caucvgprprlemdisj  7835  caucvgprprlemloc  7836  caucvgprprlemexbt  7839  caucvgprprlemaddq  7841  caucvgprprlemlim  7844  suplocexprlemss  7848  suplocexprlemrl  7850  suplocexprlemmu  7851  suplocexprlemru  7852  suplocexprlemdisj  7853  suplocexprlemloc  7854  suplocexprlemub  7856  suplocexprlemlub  7857  recexgt0sr  7906  mulgt0sr  7911  archsr  7915  caucvgsrlemoffcau  7931  suplocsrlemb  7939  suplocsrlempr  7940  suplocsrlem  7941  cnm  7965  axarch  8024  axcaucvglemcau  8031  axpre-suploclemres  8034  lelttr  8181  ltletr  8182  ltled  8211  cnegexlem1  8267  cnegexlem2  8268  renegcl  8353  negf1o  8474  gt0add  8666  apreap  8680  apirr  8698  apsym  8699  apcotr  8700  apadd1  8701  apneg  8704  mulext1  8705  mulap0r  8708  apti  8715  aprcl  8739  aptap  8743  recexap  8746  mulap0  8747  receuap  8762  mul0eqap  8763  lep1  8938  lem1  8940  letrp1  8941  recreclt  8993  lbinf  9041  suprubex  9044  nnrecgt0  9094  bndndx  9314  nn0ge2m1nn  9375  elnn0z  9405  peano2z  9428  zaddcl  9432  ztri3or0  9434  zltnle  9438  zdceq  9468  zdcle  9469  zdclt  9470  zdiv  9481  zeo  9498  fnn0ind  9509  btwnz  9512  uzm1  9699  uzp1  9702  indstr  9734  supinfneg  9736  infsupneg  9737  eluzdc  9751  nn01to3  9758  qapne  9780  xrltled  9941  xrlelttr  9948  xrltletr  9949  ge0nemnf  9966  fzdcel  10182  elfzouz2  10304  fzoss1  10315  fzospliti  10320  elincfzoext  10344  fzocatel  10350  fzostep1  10388  zsupcllemstep  10394  zsupcl  10396  infssuzledc  10399  qtri3or  10405  qltnle  10408  qdceq  10409  qdclt  10410  exbtwnzlemex  10414  rebtwn2zlemstep  10417  rebtwn2z  10419  qbtwnxr  10422  ioom  10425  ico0  10426  ioc0  10427  flqeqceilz  10485  modqadd1  10528  modqmul1  10544  frec2uzuzd  10569  frec2uzlt2d  10571  frec2uzf1od  10573  frecuzrdgrrn  10575  frec2uzrdg  10576  frecuzrdgrcl  10577  frecuzrdgsuc  10581  frecuzrdgrclt  10582  frecuzrdgdomlem  10584  uzsinds  10611  seqvalcd  10628  seqovcd  10634  seq3fveq2  10642  seqfveq2g  10644  seq3shft2  10648  seqshft2g  10649  monoord  10652  seq3split  10655  seqsplitg  10656  seq3caopr3  10658  iseqf1olemab  10669  iseqf1olemnanb  10670  iseqf1olemqk  10674  seqf1oglem1  10686  seqf1og  10688  seq3id3  10691  seq3id2  10693  seq3homo  10694  seqhomog  10697  expgt1  10744  m1expeven  10753  expnbnd  10830  expnlbnd2  10832  nn0ltexp2  10876  apexp1  10885  hashennn  10947  zfz1isolem1  11007  seq3coll  11009  pfxwrdsymbg  11166  wrdind  11198  wrd2ind  11199  cjap  11292  caucvgre  11367  cvg1nlemres  11371  resqrexlemgt0  11406  resqrexlemglsq  11408  resqrexlemga  11409  resqrtcl  11415  abslt  11474  abssubap0  11476  abssubne0  11477  caubnd2  11503  qdenre  11588  maxabslemlub  11593  maxabs  11595  maxleast  11599  fimaxre2  11613  xrmaxiflemlub  11634  xrmaxif  11637  xrmaxltsup  11644  xrmaxadd  11647  xrmineqinf  11655  climuni  11679  2clim  11687  climcn1  11694  climcn2  11695  subcn2  11697  mulcn2  11698  climsqz  11721  climsqz2  11722  climcau  11733  climcvg1nlem  11735  climcaucn  11737  serf0  11738  sumrbdclem  11763  summodclem2  11768  zsumdc  11770  divcnv  11883  absltap  11895  absgtap  11896  mertenslem2  11922  ntrivcvgap  11934  prodrbdclem  11957  prodmodclem2  11963  zproddc  11965  prodssdc  11975  fprodsplitdc  11982  fprodcl2lem  11991  efcllemp  12044  tanvalap  12094  sin01bnd  12143  cos01bnd  12144  sin01gt0  12148  absef  12156  eirrap  12164  dvds0  12192  dvdsmul1  12199  dvdsmultr1d  12218  dvdslelemd  12229  divconjdvds  12235  alzdvds  12240  3dvds  12250  sqoddm1div8z  12272  nno  12292  divalglemex  12308  bits0o  12336  dvdsbnd  12352  dvdslegcd  12360  zeqzmulgcd  12366  gcd0id  12375  gcdaddm  12380  gcd1  12383  gcdabs  12384  bezoutlemnewy  12392  bezoutlemstep  12393  bezoutlemmain  12394  bezoutlemex  12397  bezoutlemzz  12398  bezoutlemaz  12399  bezoutlembz  12400  bezoutlembi  12401  bezoutlemle  12404  bezoutlemsup  12405  mulgcd  12412  gcdzeq  12418  dvdsmulgcd  12421  sqgcd  12425  bezoutr1  12429  nninfctlemfo  12436  algcvga  12448  algfx  12449  eucalglt  12454  eucalg  12456  lcmneg  12471  lcmabs  12473  lcmgcdlem  12474  ncoprmgcdne1b  12486  mulgcddvds  12491  qredeq  12493  divgcdcoprm0  12498  cncongr1  12500  isprm2lem  12513  nprm  12520  dvdsnprmd  12522  prmdvdsfz  12536  isprm5lem  12538  coprm  12541  isprm6  12544  sqrt2irr  12559  pw2dvdslemn  12562  pw2dvdseulemle  12564  oddpwdclemdvds  12567  oddpwdclemndvds  12568  sqrt2irrap  12577  qnumdencl  12584  prmdiv  12632  modprmn0modprm0  12654  prm23lt5  12661  pythagtriplem4  12666  pythagtriplem19  12680  pythagtrip  12681  pclemub  12685  pcpre1  12690  pcpremul  12691  pceulem  12692  pcqcl  12704  pcidlem  12721  pcgcd1  12726  pc2dvds  12728  dvdsprmpweqle  12735  difsqpwdvds  12736  pcadd  12738  pcmpt  12741  expnprm  12751  pockthg  12755  infpnlem2  12758  prmunb  12760  1arith  12765  4sqlem10  12785  4sqlem11  12799  4sqlem12  12800  4sqlem13m  12801  4sqlem17  12805  4sqlem18  12806  ennnfonelemex  12860  ennnfonelemhom  12861  ennnfonelemrnh  12862  ennnfonelemnn0  12868  ennnfonelemim  12870  exmidunben  12872  ctinfomlemom  12873  ctinfom  12874  ctinf  12876  omctfn  12889  nninfdclemp1  12896  setscomd  12948  imasaddfnlemg  13221  mhmf1o  13377  grpinveu  13445  grpasscan1  13470  dfgrp3mlem  13505  grp1inv  13514  issubg4m  13604  ghmf1o  13686  srgisid  13823  ringadd2  13864  ringinvnzdiv  13887  unitgrp  13953  ringelnzr  14024  lringuplu  14033  subrguss  14073  subrgintm  14080  aprcotr  14122  islmodd  14130  lssclg  14201  lss0cl  14206  lssvneln0  14210  lss1d  14220  lmodindp1  14265  rnglidlmmgm  14333  znidomb  14495  znunit  14496  znrrg  14497  mplsubgfilemcl  14536  mplsubgfileminv  14537  tgcl  14611  neii1  14694  neii2  14696  neiss  14697  tpnei  14707  tgrest  14716  ssrest  14729  icnpimaex  14758  lmcvg  14764  cnpnei  14766  cnptopco  14769  lmff  14796  txcnp  14818  txcn  14822  hmeontr  14860  blssec  14985  mopni3  15031  blsscls2  15040  comet  15046  bdxmet  15048  bdmopn  15051  xmettxlem  15056  xmettx  15057  addcncntoplem  15108  mpomulcn  15113  mulc1cncf  15136  cncfco  15138  cncfmptc  15143  mulcncflem  15154  mulcncf  15155  dedekindeulemlu  15168  dedekindeulemeu  15169  suplociccreex  15171  suplociccex  15172  dedekindicclemlu  15177  dedekindicclemeu  15178  ivthinclemlopn  15183  ivthinclemlr  15184  ivthinclemuopn  15185  ivthinclemur  15186  ivthinclemloc  15188  ivthinc  15190  ivthreinc  15192  ivthdichlem  15198  limcimolemlt  15211  limcresi  15213  cnplimcim  15214  cnplimclemle  15215  cnplimclemr  15216  limccnpcntop  15222  limccoap  15225  dvcoapbr  15254  dvcj  15256  plyf  15284  plyaddlem1  15294  plymullem1  15295  plyco  15306  plycj  15308  plycn  15309  plyrecj  15310  dvply2g  15313  efltlemlt  15321  sin0pilem2  15329  tangtx  15385  logdivlti  15428  rplogbval  15492  logbgcd1irraplemexp  15515  logbgcd1irraplemap  15516  logbgcd1irrap  15517  perfect1  15545  perfectlem1  15546  perfectlem2  15547  lgsval4a  15574  lgsdir2lem3  15582  lgsne0  15590  gausslemma2dlem3  15615  gausslemma2dlem4  15616  gausslemma2dlem6  15619  gausslemma2dlem7  15620  gausslemma2d  15621  lgseisenlem1  15622  lgsquadlem2  15630  lgsquadlem3  15631  lgsquad2lem2  15634  lgsquad3  15636  2lgsoddprmlem2  15658  2sqlem8a  15674  2sqlem8  15675  2sqlem9  15676  lpvtx  15750  upgrex  15774  bj-exlimmpi  15845  uzdcinzz  15873  bj-charfundcALT  15883  bj-2inf  16012  bj-peano4  16029  bj-nn0suc  16038  1dom1el  16065  subctctexmid  16078  nninfalllem1  16086  nninfsellemqall  16093  nninfomnilem  16096  nninffeq  16098  nnnninfex  16100  exmidsbthrlem  16102  sbthomlem  16105  refeq  16108  isomninnlem  16110  apdifflemr  16127  redcwlpo  16135  reap0  16138  nconstwlpolem  16145