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  623  mt2d  628  mpnanrd  697  mpjaod  723  stdcndcOLD  851  impidc  863  jadc  868  pm2.54dc  896  oplem1  981  mp3and  1374  xor3dc  1429  exlimdd  1918  exlimddv  1945  eqrdav  2228  necon1aidc  2451  necon1bidc  2452  necon4aidc  2468  reximddv  2633  reximssdv  2634  rexlimddv  2653  vtoclgft  2851  rspcedvd  2913  sseldd  3225  ssneldd  3227  tpid3g  3781  preq12b  3847  axpweq  4254  exmid1dc  4283  exmid1stab  4291  opth  4322  issod  4409  frirrg  4440  frind  4442  ralxfr2d  4554  rexxfr2d  4555  eldifpw  4567  onun2  4581  onuni  4585  elirr  4632  en2lp  4645  wetriext  4668  peano2  4686  relop  4871  elres  5040  sotri2  5125  iota4an  5298  iota5  5299  funeu  5342  funopg  5351  imadiflem  5399  funimaexglem  5403  ssimaex  5694  ffvelcdm  5767  dff3im  5779  dffo4  5782  funopsn  5816  f1eqcocnv  5914  f1oiso2  5950  riota5f  5980  riotass2  5982  acexmidlemcase  5995  elovimad  6044  ovmpodf  6135  ovmpodv2  6137  ovi3  6141  ov6g  6142  caoftrn  6249  op1steq  6323  tfr0dm  6466  tfrlemibxssdm  6471  tfrlemi14d  6477  tfr1onlembxssdm  6487  tfr1onlemaccex  6492  tfr1onlemres  6493  tfrcllembxssdm  6500  tfrcllemaccex  6505  tfrcllemres  6506  rdgivallem  6525  nnsucelsuc  6635  nnsucsssuc  6636  dcdifsnid  6648  nnawordex  6673  ersym  6690  mapvalg  6803  pmvalg  6804  mapsn  6835  fundmen  6957  en2  6971  pw2f1odclem  6991  mapdom1g  7004  fidceq  7027  fin0or  7044  findcard2  7047  findcard2s  7048  prfidceq  7086  fiintim  7089  suplub2ti  7164  supsnti  7168  supisoex  7172  difinfsnlem  7262  difinfsn  7263  ctm  7272  ctssdclemn0  7273  ctssdccl  7274  ctssdc  7276  enumctlemm  7277  nninfninc  7286  nnnninfeq2  7292  enomnilem  7301  exmidomniim  7304  exmidomni  7305  fodjuomnilemdc  7307  fodjuomnilemres  7311  omnimkv  7319  mkvprop  7321  omniwomnimkv  7330  en2prde  7362  pr2cv1  7364  en2eleq  7369  acfun  7385  exmidontriimlem1  7399  exmidontriimlem4  7402  exmidontriim  7403  ccfunen  7446  cc4f  7451  cc4n  7453  elni2  7497  mulclpi  7511  nlt1pig  7524  indpi  7525  recclnq  7575  ltexnqq  7591  halfnqq  7593  prarloclemarch  7601  prarloclemarch2  7602  prop  7658  prltlu  7670  prarloclem3step  7679  prarloclem5  7683  prarloclem  7684  prarloc  7686  prarloc2  7687  genpml  7700  genpmu  7701  genprndl  7704  genprndu  7705  genpdisj  7706  addnqprllem  7710  addnqprulem  7711  addlocprlemeq  7716  addlocprlemgt  7717  addlocprlem  7718  addlocpr  7719  nqprloc  7728  nqprl  7734  nqpru  7735  addnqprlemrl  7740  addnqprlemru  7741  appdivnq  7746  prmuloc  7749  prmuloc2  7750  mullocprlem  7753  mullocpr  7754  mulnqprlemrl  7756  mulnqprlemru  7757  ltprordil  7772  ltpopr  7778  ltsopr  7779  ltaddpr  7780  ltexprlemm  7783  ltexprlemopl  7784  ltexprlemlol  7785  ltexprlemopu  7786  ltexprlemupu  7787  ltexprlemloc  7790  ltexprlemfl  7792  ltexprlemrl  7793  ltexprlemfu  7794  ltexprlemru  7795  ltaprg  7802  recexprlemm  7807  recexprlem1ssl  7816  recexprlem1ssu  7817  aptiprleml  7822  aptiprlemu  7823  archpr  7826  cauappcvgprlemm  7828  cauappcvgprlemopl  7829  cauappcvgprlemlol  7830  cauappcvgprlemopu  7831  cauappcvgprlemupu  7832  cauappcvgprlemdisj  7834  cauappcvgprlemloc  7835  cauappcvgprlemladdfu  7837  cauappcvgprlemladdfl  7838  cauappcvgprlemladdru  7839  cauappcvgprlem1  7842  archrecpr  7847  caucvgprlemnkj  7849  caucvgprlemnbj  7850  caucvgprlemm  7851  caucvgprlemopl  7852  caucvgprlemlol  7853  caucvgprlemopu  7854  caucvgprlemupu  7855  caucvgprlemdisj  7857  caucvgprlemloc  7858  caucvgprlemladdfu  7860  caucvgprlem1  7862  caucvgprlemlim  7864  caucvgprprlemnbj  7876  caucvgprprlemml  7877  caucvgprprlemopl  7880  caucvgprprlemlol  7881  caucvgprprlemopu  7882  caucvgprprlemupu  7883  caucvgprprlemdisj  7885  caucvgprprlemloc  7886  caucvgprprlemexbt  7889  caucvgprprlemaddq  7891  caucvgprprlemlim  7894  suplocexprlemss  7898  suplocexprlemrl  7900  suplocexprlemmu  7901  suplocexprlemru  7902  suplocexprlemdisj  7903  suplocexprlemloc  7904  suplocexprlemub  7906  suplocexprlemlub  7907  recexgt0sr  7956  mulgt0sr  7961  archsr  7965  caucvgsrlemoffcau  7981  suplocsrlemb  7989  suplocsrlempr  7990  suplocsrlem  7991  cnm  8015  axarch  8074  axcaucvglemcau  8081  axpre-suploclemres  8084  lelttr  8231  ltletr  8232  ltled  8261  cnegexlem1  8317  cnegexlem2  8318  renegcl  8403  negf1o  8524  gt0add  8716  apreap  8730  apirr  8748  apsym  8749  apcotr  8750  apadd1  8751  apneg  8754  mulext1  8755  mulap0r  8758  apti  8765  aprcl  8789  aptap  8793  recexap  8796  mulap0  8797  receuap  8812  mul0eqap  8813  lep1  8988  lem1  8990  letrp1  8991  recreclt  9043  lbinf  9091  suprubex  9094  nnrecgt0  9144  bndndx  9364  nn0ge2m1nn  9425  elnn0z  9455  peano2z  9478  zaddcl  9482  ztri3or0  9484  zltnle  9488  zdceq  9518  zdcle  9519  zdclt  9520  zdiv  9531  zeo  9548  fnn0ind  9559  btwnz  9562  uzm1  9749  uzp1  9752  indstr  9784  supinfneg  9786  infsupneg  9787  eluzdc  9801  nn01to3  9808  qapne  9830  xrltled  9991  xrlelttr  9998  xrltletr  9999  ge0nemnf  10016  fzdcel  10232  elfzouz2  10354  fzoss1  10365  fzospliti  10370  elincfzoext  10394  fzocatel  10400  fzostep1  10438  zsupcllemstep  10444  zsupcl  10446  infssuzledc  10449  qtri3or  10455  qltnle  10458  qdceq  10459  qdclt  10460  exbtwnzlemex  10464  rebtwn2zlemstep  10467  rebtwn2z  10469  qbtwnxr  10472  ioom  10475  ico0  10476  ioc0  10477  flqeqceilz  10535  modqadd1  10578  modqmul1  10594  frec2uzuzd  10619  frec2uzlt2d  10621  frec2uzf1od  10623  frecuzrdgrrn  10625  frec2uzrdg  10626  frecuzrdgrcl  10627  frecuzrdgsuc  10631  frecuzrdgrclt  10632  frecuzrdgdomlem  10634  uzsinds  10661  seqvalcd  10678  seqovcd  10684  seq3fveq2  10692  seqfveq2g  10694  seq3shft2  10698  seqshft2g  10699  monoord  10702  seq3split  10705  seqsplitg  10706  seq3caopr3  10708  iseqf1olemab  10719  iseqf1olemnanb  10720  iseqf1olemqk  10724  seqf1oglem1  10736  seqf1og  10738  seq3id3  10741  seq3id2  10743  seq3homo  10744  seqhomog  10747  expgt1  10794  m1expeven  10803  expnbnd  10880  expnlbnd2  10882  nn0ltexp2  10926  apexp1  10935  hashennn  10997  zfz1isolem1  11057  seq3coll  11059  pfxwrdsymbg  11217  wrdind  11249  wrd2ind  11250  cjap  11412  caucvgre  11487  cvg1nlemres  11491  resqrexlemgt0  11526  resqrexlemglsq  11528  resqrexlemga  11529  resqrtcl  11535  abslt  11594  abssubap0  11596  abssubne0  11597  caubnd2  11623  qdenre  11708  maxabslemlub  11713  maxabs  11715  maxleast  11719  fimaxre2  11733  xrmaxiflemlub  11754  xrmaxif  11757  xrmaxltsup  11764  xrmaxadd  11767  xrmineqinf  11775  climuni  11799  2clim  11807  climcn1  11814  climcn2  11815  subcn2  11817  mulcn2  11818  climsqz  11841  climsqz2  11842  climcau  11853  climcvg1nlem  11855  climcaucn  11857  serf0  11858  sumrbdclem  11883  summodclem2  11888  zsumdc  11890  divcnv  12003  absltap  12015  absgtap  12016  mertenslem2  12042  ntrivcvgap  12054  prodrbdclem  12077  prodmodclem2  12083  zproddc  12085  prodssdc  12095  fprodsplitdc  12102  fprodcl2lem  12111  efcllemp  12164  tanvalap  12214  sin01bnd  12263  cos01bnd  12264  sin01gt0  12268  absef  12276  eirrap  12284  dvds0  12312  dvdsmul1  12319  dvdsmultr1d  12338  dvdslelemd  12349  divconjdvds  12355  alzdvds  12360  3dvds  12370  sqoddm1div8z  12392  nno  12412  divalglemex  12428  bits0o  12456  dvdsbnd  12472  dvdslegcd  12480  zeqzmulgcd  12486  gcd0id  12495  gcdaddm  12500  gcd1  12503  gcdabs  12504  bezoutlemnewy  12512  bezoutlemstep  12513  bezoutlemmain  12514  bezoutlemex  12517  bezoutlemzz  12518  bezoutlemaz  12519  bezoutlembz  12520  bezoutlembi  12521  bezoutlemle  12524  bezoutlemsup  12525  mulgcd  12532  gcdzeq  12538  dvdsmulgcd  12541  sqgcd  12545  bezoutr1  12549  nninfctlemfo  12556  algcvga  12568  algfx  12569  eucalglt  12574  eucalg  12576  lcmneg  12591  lcmabs  12593  lcmgcdlem  12594  ncoprmgcdne1b  12606  mulgcddvds  12611  qredeq  12613  divgcdcoprm0  12618  cncongr1  12620  isprm2lem  12633  nprm  12640  dvdsnprmd  12642  prmdvdsfz  12656  isprm5lem  12658  coprm  12661  isprm6  12664  sqrt2irr  12679  pw2dvdslemn  12682  pw2dvdseulemle  12684  oddpwdclemdvds  12687  oddpwdclemndvds  12688  sqrt2irrap  12697  qnumdencl  12704  prmdiv  12752  modprmn0modprm0  12774  prm23lt5  12781  pythagtriplem4  12786  pythagtriplem19  12800  pythagtrip  12801  pclemub  12805  pcpre1  12810  pcpremul  12811  pceulem  12812  pcqcl  12824  pcidlem  12841  pcgcd1  12846  pc2dvds  12848  dvdsprmpweqle  12855  difsqpwdvds  12856  pcadd  12858  pcmpt  12861  expnprm  12871  pockthg  12875  infpnlem2  12878  prmunb  12880  1arith  12885  4sqlem10  12905  4sqlem11  12919  4sqlem12  12920  4sqlem13m  12921  4sqlem17  12925  4sqlem18  12926  ennnfonelemex  12980  ennnfonelemhom  12981  ennnfonelemrnh  12982  ennnfonelemnn0  12988  ennnfonelemim  12990  exmidunben  12992  ctinfomlemom  12993  ctinfom  12994  ctinf  12996  omctfn  13009  nninfdclemp1  13016  setscomd  13068  imasaddfnlemg  13342  mhmf1o  13498  grpinveu  13566  grpasscan1  13591  dfgrp3mlem  13626  grp1inv  13635  issubg4m  13725  ghmf1o  13807  srgisid  13944  ringadd2  13985  ringinvnzdiv  14008  unitgrp  14074  ringelnzr  14145  lringuplu  14154  subrguss  14194  subrgintm  14201  aprcotr  14243  islmodd  14251  lssclg  14322  lss0cl  14327  lssvneln0  14331  lss1d  14341  lmodindp1  14386  rnglidlmmgm  14454  znidomb  14616  znunit  14617  znrrg  14618  mplsubgfilemcl  14657  mplsubgfileminv  14658  tgcl  14732  neii1  14815  neii2  14817  neiss  14818  tpnei  14828  tgrest  14837  ssrest  14850  icnpimaex  14879  lmcvg  14885  cnpnei  14887  cnptopco  14890  lmff  14917  txcnp  14939  txcn  14943  hmeontr  14981  blssec  15106  mopni3  15152  blsscls2  15161  comet  15167  bdxmet  15169  bdmopn  15172  xmettxlem  15177  xmettx  15178  addcncntoplem  15229  mpomulcn  15234  mulc1cncf  15257  cncfco  15259  cncfmptc  15264  mulcncflem  15275  mulcncf  15276  dedekindeulemlu  15289  dedekindeulemeu  15290  suplociccreex  15292  suplociccex  15293  dedekindicclemlu  15298  dedekindicclemeu  15299  ivthinclemlopn  15304  ivthinclemlr  15305  ivthinclemuopn  15306  ivthinclemur  15307  ivthinclemloc  15309  ivthinc  15311  ivthreinc  15313  ivthdichlem  15319  limcimolemlt  15332  limcresi  15334  cnplimcim  15335  cnplimclemle  15336  cnplimclemr  15337  limccnpcntop  15343  limccoap  15346  dvcoapbr  15375  dvcj  15377  plyf  15405  plyaddlem1  15415  plymullem1  15416  plyco  15427  plycj  15429  plycn  15430  plyrecj  15431  dvply2g  15434  efltlemlt  15442  sin0pilem2  15450  tangtx  15506  logdivlti  15549  rplogbval  15613  logbgcd1irraplemexp  15636  logbgcd1irraplemap  15637  logbgcd1irrap  15638  perfect1  15666  perfectlem1  15667  perfectlem2  15668  lgsval4a  15695  lgsdir2lem3  15703  lgsne0  15711  gausslemma2dlem3  15736  gausslemma2dlem4  15737  gausslemma2dlem6  15740  gausslemma2dlem7  15741  gausslemma2d  15742  lgseisenlem1  15743  lgsquadlem2  15751  lgsquadlem3  15752  lgsquad2lem2  15755  lgsquad3  15757  2lgsoddprmlem2  15779  2sqlem8a  15795  2sqlem8  15796  2sqlem9  15797  lpvtx  15873  upgrex  15897  edgupgren  15933  umgredg  15937  upgrpredgv  15938  upgredg2vtx  15940  upgredgpr  15941  uspgrf1oedg  15968  usgredg4  16007  uspgredgdomord  16021  wlkvtxiedgg  16042  bj-exlimmpi  16092  uzdcinzz  16120  bj-charfundcALT  16130  bj-2inf  16259  bj-peano4  16276  bj-nn0suc  16285  1dom1el  16312  subctctexmid  16325  nninfalllem1  16333  nninfsellemqall  16340  nninfomnilem  16343  nninffeq  16345  nnnninfex  16347  exmidsbthrlem  16349  sbthomlem  16352  refeq  16355  isomninnlem  16357  apdifflemr  16374  redcwlpo  16382  reap0  16385  nconstwlpolem  16392