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  146  mpbird  166  jcai  309  mp2and  430  pm2.21dd  610  mt2d  615  mpjaod  708  stdcndcOLD  836  impidc  848  jadc  853  pm2.54dc  881  pm4.55dc  928  oplem1  965  mp3and  1330  xor3dc  1377  exlimdd  1860  exlimddv  1886  eqrdav  2164  necon1aidc  2387  necon1bidc  2388  necon4aidc  2404  reximddv  2569  reximssdv  2570  rexlimddv  2588  vtoclgft  2776  rspcedvd  2836  sseldd  3143  ssneldd  3145  tpid3g  3691  preq12b  3750  axpweq  4150  exmid1dc  4179  opth  4215  issod  4297  frirrg  4328  frind  4330  ralxfr2d  4442  rexxfr2d  4443  eldifpw  4455  onun2  4467  onuni  4471  elirr  4518  en2lp  4531  wetriext  4554  peano2  4572  relop  4754  elres  4920  sotri2  5001  iota4an  5172  iota5  5173  funeu  5213  funopg  5222  imadiflem  5267  funimaexglem  5271  ssimaex  5547  ffvelrn  5618  dff3im  5630  dffo4  5633  f1eqcocnv  5759  f1oiso2  5795  riota5f  5822  riotass2  5824  acexmidlemcase  5837  ovmpodf  5973  ovmpodv2  5975  ovi3  5978  ov6g  5979  caoftrn  6075  op1steq  6147  tfr0dm  6290  tfrlemibxssdm  6295  tfrlemi14d  6301  tfr1onlembxssdm  6311  tfr1onlemaccex  6316  tfr1onlemres  6317  tfrcllembxssdm  6324  tfrcllemaccex  6329  tfrcllemres  6330  rdgivallem  6349  nnsucelsuc  6459  nnsucsssuc  6460  dcdifsnid  6472  nnawordex  6496  ersym  6513  mapvalg  6624  pmvalg  6625  mapsn  6656  fundmen  6772  mapdom1g  6813  fidceq  6835  fin0or  6852  findcard2  6855  findcard2s  6856  fiintim  6894  suplub2ti  6966  supsnti  6970  supisoex  6974  difinfsnlem  7064  difinfsn  7065  ctm  7074  ctssdclemn0  7075  ctssdccl  7076  ctssdc  7078  enumctlemm  7079  nnnninfeq2  7093  enomnilem  7102  exmidomniim  7105  exmidomni  7106  fodjuomnilemdc  7108  fodjuomnilemres  7112  omnimkv  7120  mkvprop  7122  omniwomnimkv  7131  en2eleq  7151  acfun  7163  exmidontriimlem1  7177  exmidontriimlem4  7180  exmidontriim  7181  ccfunen  7205  cc4f  7210  cc4n  7212  elni2  7255  mulclpi  7269  nlt1pig  7282  indpi  7283  recclnq  7333  ltexnqq  7349  halfnqq  7351  prarloclemarch  7359  prarloclemarch2  7360  prop  7416  prltlu  7428  prarloclem3step  7437  prarloclem5  7441  prarloclem  7442  prarloc  7444  prarloc2  7445  genpml  7458  genpmu  7459  genprndl  7462  genprndu  7463  genpdisj  7464  addnqprllem  7468  addnqprulem  7469  addlocprlemeq  7474  addlocprlemgt  7475  addlocprlem  7476  addlocpr  7477  nqprloc  7486  nqprl  7492  nqpru  7493  addnqprlemrl  7498  addnqprlemru  7499  appdivnq  7504  prmuloc  7507  prmuloc2  7508  mullocprlem  7511  mullocpr  7512  mulnqprlemrl  7514  mulnqprlemru  7515  ltprordil  7530  ltpopr  7536  ltsopr  7537  ltaddpr  7538  ltexprlemm  7541  ltexprlemopl  7542  ltexprlemlol  7543  ltexprlemopu  7544  ltexprlemupu  7545  ltexprlemloc  7548  ltexprlemfl  7550  ltexprlemrl  7551  ltexprlemfu  7552  ltexprlemru  7553  ltaprg  7560  recexprlemm  7565  recexprlem1ssl  7574  recexprlem1ssu  7575  aptiprleml  7580  aptiprlemu  7581  archpr  7584  cauappcvgprlemm  7586  cauappcvgprlemopl  7587  cauappcvgprlemlol  7588  cauappcvgprlemopu  7589  cauappcvgprlemupu  7590  cauappcvgprlemdisj  7592  cauappcvgprlemloc  7593  cauappcvgprlemladdfu  7595  cauappcvgprlemladdfl  7596  cauappcvgprlemladdru  7597  cauappcvgprlem1  7600  archrecpr  7605  caucvgprlemnkj  7607  caucvgprlemnbj  7608  caucvgprlemm  7609  caucvgprlemopl  7610  caucvgprlemlol  7611  caucvgprlemopu  7612  caucvgprlemupu  7613  caucvgprlemdisj  7615  caucvgprlemloc  7616  caucvgprlemladdfu  7618  caucvgprlem1  7620  caucvgprlemlim  7622  caucvgprprlemnbj  7634  caucvgprprlemml  7635  caucvgprprlemopl  7638  caucvgprprlemlol  7639  caucvgprprlemopu  7640  caucvgprprlemupu  7641  caucvgprprlemdisj  7643  caucvgprprlemloc  7644  caucvgprprlemexbt  7647  caucvgprprlemaddq  7649  caucvgprprlemlim  7652  suplocexprlemss  7656  suplocexprlemrl  7658  suplocexprlemmu  7659  suplocexprlemru  7660  suplocexprlemdisj  7661  suplocexprlemloc  7662  suplocexprlemub  7664  suplocexprlemlub  7665  recexgt0sr  7714  mulgt0sr  7719  archsr  7723  caucvgsrlemoffcau  7739  suplocsrlemb  7747  suplocsrlempr  7748  suplocsrlem  7749  cnm  7773  axarch  7832  axcaucvglemcau  7839  axpre-suploclemres  7842  lelttr  7987  ltletr  7988  ltled  8017  cnegexlem1  8073  cnegexlem2  8074  renegcl  8159  negf1o  8280  gt0add  8471  apreap  8485  apirr  8503  apsym  8504  apcotr  8505  apadd1  8506  apneg  8509  mulext1  8510  mulap0r  8513  apti  8520  aprcl  8544  recexap  8550  mulap0  8551  receuap  8566  mul0eqap  8567  lep1  8740  lem1  8742  letrp1  8743  recreclt  8795  lbinf  8843  suprubex  8846  nnrecgt0  8895  bndndx  9113  nn0ge2m1nn  9174  elnn0z  9204  peano2z  9227  zaddcl  9231  ztri3or0  9233  zltnle  9237  zdceq  9266  zdcle  9267  zdclt  9268  zdiv  9279  zeo  9296  fnn0ind  9307  btwnz  9310  uzm1  9496  uzp1  9499  indstr  9531  supinfneg  9533  infsupneg  9534  eluzdc  9548  nn01to3  9555  qapne  9577  xrltled  9735  xrlelttr  9742  xrltletr  9743  ge0nemnf  9760  fzdcel  9975  elfzouz2  10096  fzoss1  10106  fzospliti  10111  fzocatel  10134  fzostep1  10172  qtri3or  10178  qltnle  10181  qdceq  10182  exbtwnzlemex  10185  rebtwn2zlemstep  10188  rebtwn2z  10190  qbtwnxr  10193  ioom  10196  ico0  10197  ioc0  10198  flqeqceilz  10253  modqadd1  10296  modqmul1  10312  frec2uzuzd  10337  frec2uzlt2d  10339  frec2uzf1od  10341  frecuzrdgrrn  10343  frec2uzrdg  10344  frecuzrdgrcl  10345  frecuzrdgsuc  10349  frecuzrdgrclt  10350  frecuzrdgdomlem  10352  uzsinds  10377  seqvalcd  10394  seqovcd  10398  seq3fveq2  10404  seq3shft2  10408  monoord  10411  seq3split  10414  seq3caopr3  10416  iseqf1olemab  10424  iseqf1olemnanb  10425  iseqf1olemqk  10429  seq3id3  10442  seq3id2  10444  seq3homo  10445  expgt1  10493  m1expeven  10502  expnbnd  10578  expnlbnd2  10580  nn0ltexp2  10623  apexp1  10631  hashennn  10693  zfz1isolem1  10753  seq3coll  10755  cjap  10848  caucvgre  10923  cvg1nlemres  10927  resqrexlemgt0  10962  resqrexlemglsq  10964  resqrexlemga  10965  resqrtcl  10971  abslt  11030  abssubap0  11032  abssubne0  11033  caubnd2  11059  qdenre  11144  maxabslemlub  11149  maxabs  11151  maxleast  11155  fimaxre2  11168  xrmaxiflemlub  11189  xrmaxif  11192  xrmaxltsup  11199  xrmaxadd  11202  xrmineqinf  11210  climuni  11234  2clim  11242  climcn1  11249  climcn2  11250  subcn2  11252  mulcn2  11253  climsqz  11276  climsqz2  11277  climcau  11288  climcvg1nlem  11290  climcaucn  11292  serf0  11293  sumrbdclem  11318  summodclem2  11323  zsumdc  11325  divcnv  11438  absltap  11450  absgtap  11451  mertenslem2  11477  ntrivcvgap  11489  prodrbdclem  11512  prodmodclem2  11518  zproddc  11520  prodssdc  11530  fprodsplitdc  11537  fprodcl2lem  11546  efcllemp  11599  tanvalap  11649  sin01bnd  11698  cos01bnd  11699  sin01gt0  11702  absef  11710  eirrap  11718  dvds0  11746  dvdsmul1  11753  dvdsmultr1d  11772  dvdslelemd  11781  divconjdvds  11787  alzdvds  11792  sqoddm1div8z  11823  nno  11843  divalglemex  11859  zsupcllemstep  11878  zsupcl  11880  infssuzledc  11883  dvdsbnd  11889  dvdslegcd  11897  zeqzmulgcd  11903  gcd0id  11912  gcdaddm  11917  gcd1  11920  gcdabs  11921  bezoutlemnewy  11929  bezoutlemstep  11930  bezoutlemmain  11931  bezoutlemex  11934  bezoutlemzz  11935  bezoutlemaz  11936  bezoutlembz  11937  bezoutlembi  11938  bezoutlemle  11941  bezoutlemsup  11942  mulgcd  11949  gcdzeq  11955  dvdsmulgcd  11958  sqgcd  11962  bezoutr1  11966  algcvga  11983  algfx  11984  eucalglt  11989  eucalg  11991  lcmneg  12006  lcmabs  12008  lcmgcdlem  12009  ncoprmgcdne1b  12021  mulgcddvds  12026  qredeq  12028  divgcdcoprm0  12033  cncongr1  12035  isprm2lem  12048  nprm  12055  dvdsnprmd  12057  prmdvdsfz  12071  isprm5lem  12073  coprm  12076  isprm6  12079  sqrt2irr  12094  pw2dvdslemn  12097  pw2dvdseulemle  12099  oddpwdclemdvds  12102  oddpwdclemndvds  12103  sqrt2irrap  12112  qnumdencl  12119  prmdiv  12167  modprmn0modprm0  12188  prm23lt5  12195  pythagtriplem4  12200  pythagtriplem19  12214  pythagtrip  12215  pclemub  12219  pcpre1  12224  pcpremul  12225  pceulem  12226  pcqcl  12238  pcidlem  12254  pcgcd1  12259  pc2dvds  12261  dvdsprmpweqle  12268  difsqpwdvds  12269  pcadd  12271  pcmpt  12273  expnprm  12283  pockthg  12287  infpnlem2  12290  prmunb  12292  1arith  12297  4sqlem10  12317  ennnfonelemex  12347  ennnfonelemhom  12348  ennnfonelemrnh  12349  ennnfonelemnn0  12355  ennnfonelemim  12357  exmidunben  12359  ctinfomlemom  12360  ctinfom  12361  ctinf  12363  omctfn  12376  nninfdclemp1  12383  tgcl  12704  neii1  12787  neii2  12789  neiss  12790  tpnei  12800  tgrest  12809  ssrest  12822  icnpimaex  12851  lmcvg  12857  cnpnei  12859  cnptopco  12862  lmff  12889  txcnp  12911  txcn  12915  hmeontr  12953  blssec  13078  mopni3  13124  blsscls2  13133  comet  13139  bdxmet  13141  bdmopn  13144  xmettxlem  13149  xmettx  13150  addcncntoplem  13191  mulc1cncf  13216  cncfco  13218  cncfmptc  13222  mulcncflem  13230  mulcncf  13231  dedekindeulemlu  13239  dedekindeulemeu  13240  suplociccreex  13242  suplociccex  13243  dedekindicclemlu  13248  dedekindicclemeu  13249  ivthinclemlopn  13254  ivthinclemlr  13255  ivthinclemuopn  13256  ivthinclemur  13257  ivthinclemloc  13259  ivthinc  13261  limcimolemlt  13273  limcresi  13275  cnplimcim  13276  cnplimclemle  13277  cnplimclemr  13278  limccnpcntop  13284  limccoap  13287  dvcoapbr  13311  dvcj  13313  efltlemlt  13335  sin0pilem2  13343  tangtx  13399  logdivlti  13442  rplogbval  13503  logbgcd1irraplemexp  13526  logbgcd1irraplemap  13527  logbgcd1irrap  13528  lgsval4a  13563  lgsdir2lem3  13571  lgsne0  13579  2sqlem8a  13598  2sqlem8  13599  2sqlem9  13600  bj-exlimmpi  13651  uzdcinzz  13679  bj-charfundcALT  13691  bj-2inf  13820  bj-peano4  13837  bj-nn0suc  13846  exmid1stab  13880  subctctexmid  13881  nninfalllem1  13888  nninfsellemqall  13895  nninfomnilem  13898  nninffeq  13900  exmidsbthrlem  13901  sbthomlem  13904  refeq  13907  isomninnlem  13909  apdifflemr  13926  redcwlpo  13934  reap0  13937  nconstwlpolem  13943