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  7274  acfun  7290  exmidontriimlem1  7304  exmidontriimlem4  7307  exmidontriim  7308  ccfunen  7347  cc4f  7352  cc4n  7354  elni2  7398  mulclpi  7412  nlt1pig  7425  indpi  7426  recclnq  7476  ltexnqq  7492  halfnqq  7494  prarloclemarch  7502  prarloclemarch2  7503  prop  7559  prltlu  7571  prarloclem3step  7580  prarloclem5  7584  prarloclem  7585  prarloc  7587  prarloc2  7588  genpml  7601  genpmu  7602  genprndl  7605  genprndu  7606  genpdisj  7607  addnqprllem  7611  addnqprulem  7612  addlocprlemeq  7617  addlocprlemgt  7618  addlocprlem  7619  addlocpr  7620  nqprloc  7629  nqprl  7635  nqpru  7636  addnqprlemrl  7641  addnqprlemru  7642  appdivnq  7647  prmuloc  7650  prmuloc2  7651  mullocprlem  7654  mullocpr  7655  mulnqprlemrl  7657  mulnqprlemru  7658  ltprordil  7673  ltpopr  7679  ltsopr  7680  ltaddpr  7681  ltexprlemm  7684  ltexprlemopl  7685  ltexprlemlol  7686  ltexprlemopu  7687  ltexprlemupu  7688  ltexprlemloc  7691  ltexprlemfl  7693  ltexprlemrl  7694  ltexprlemfu  7695  ltexprlemru  7696  ltaprg  7703  recexprlemm  7708  recexprlem1ssl  7717  recexprlem1ssu  7718  aptiprleml  7723  aptiprlemu  7724  archpr  7727  cauappcvgprlemm  7729  cauappcvgprlemopl  7730  cauappcvgprlemlol  7731  cauappcvgprlemopu  7732  cauappcvgprlemupu  7733  cauappcvgprlemdisj  7735  cauappcvgprlemloc  7736  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  cauappcvgprlemladdru  7740  cauappcvgprlem1  7743  archrecpr  7748  caucvgprlemnkj  7750  caucvgprlemnbj  7751  caucvgprlemm  7752  caucvgprlemopl  7753  caucvgprlemlol  7754  caucvgprlemopu  7755  caucvgprlemupu  7756  caucvgprlemdisj  7758  caucvgprlemloc  7759  caucvgprlemladdfu  7761  caucvgprlem1  7763  caucvgprlemlim  7765  caucvgprprlemnbj  7777  caucvgprprlemml  7778  caucvgprprlemopl  7781  caucvgprprlemlol  7782  caucvgprprlemopu  7783  caucvgprprlemupu  7784  caucvgprprlemdisj  7786  caucvgprprlemloc  7787  caucvgprprlemexbt  7790  caucvgprprlemaddq  7792  caucvgprprlemlim  7795  suplocexprlemss  7799  suplocexprlemrl  7801  suplocexprlemmu  7802  suplocexprlemru  7803  suplocexprlemdisj  7804  suplocexprlemloc  7805  suplocexprlemub  7807  suplocexprlemlub  7808  recexgt0sr  7857  mulgt0sr  7862  archsr  7866  caucvgsrlemoffcau  7882  suplocsrlemb  7890  suplocsrlempr  7891  suplocsrlem  7892  cnm  7916  axarch  7975  axcaucvglemcau  7982  axpre-suploclemres  7985  lelttr  8132  ltletr  8133  ltled  8162  cnegexlem1  8218  cnegexlem2  8219  renegcl  8304  negf1o  8425  gt0add  8617  apreap  8631  apirr  8649  apsym  8650  apcotr  8651  apadd1  8652  apneg  8655  mulext1  8656  mulap0r  8659  apti  8666  aprcl  8690  aptap  8694  recexap  8697  mulap0  8698  receuap  8713  mul0eqap  8714  lep1  8889  lem1  8891  letrp1  8892  recreclt  8944  lbinf  8992  suprubex  8995  nnrecgt0  9045  bndndx  9265  nn0ge2m1nn  9326  elnn0z  9356  peano2z  9379  zaddcl  9383  ztri3or0  9385  zltnle  9389  zdceq  9418  zdcle  9419  zdclt  9420  zdiv  9431  zeo  9448  fnn0ind  9459  btwnz  9462  uzm1  9649  uzp1  9652  indstr  9684  supinfneg  9686  infsupneg  9687  eluzdc  9701  nn01to3  9708  qapne  9730  xrltled  9891  xrlelttr  9898  xrltletr  9899  ge0nemnf  9916  fzdcel  10132  elfzouz2  10254  fzoss1  10264  fzospliti  10269  fzocatel  10292  fzostep1  10330  zsupcllemstep  10336  zsupcl  10338  infssuzledc  10341  qtri3or  10347  qltnle  10350  qdceq  10351  qdclt  10352  exbtwnzlemex  10356  rebtwn2zlemstep  10359  rebtwn2z  10361  qbtwnxr  10364  ioom  10367  ico0  10368  ioc0  10369  flqeqceilz  10427  modqadd1  10470  modqmul1  10486  frec2uzuzd  10511  frec2uzlt2d  10513  frec2uzf1od  10515  frecuzrdgrrn  10517  frec2uzrdg  10518  frecuzrdgrcl  10519  frecuzrdgsuc  10523  frecuzrdgrclt  10524  frecuzrdgdomlem  10526  uzsinds  10553  seqvalcd  10570  seqovcd  10576  seq3fveq2  10584  seqfveq2g  10586  seq3shft2  10590  seqshft2g  10591  monoord  10594  seq3split  10597  seqsplitg  10598  seq3caopr3  10600  iseqf1olemab  10611  iseqf1olemnanb  10612  iseqf1olemqk  10616  seqf1oglem1  10628  seqf1og  10630  seq3id3  10633  seq3id2  10635  seq3homo  10636  seqhomog  10639  expgt1  10686  m1expeven  10695  expnbnd  10772  expnlbnd2  10774  nn0ltexp2  10818  apexp1  10827  hashennn  10889  zfz1isolem1  10949  seq3coll  10951  cjap  11088  caucvgre  11163  cvg1nlemres  11167  resqrexlemgt0  11202  resqrexlemglsq  11204  resqrexlemga  11205  resqrtcl  11211  abslt  11270  abssubap0  11272  abssubne0  11273  caubnd2  11299  qdenre  11384  maxabslemlub  11389  maxabs  11391  maxleast  11395  fimaxre2  11409  xrmaxiflemlub  11430  xrmaxif  11433  xrmaxltsup  11440  xrmaxadd  11443  xrmineqinf  11451  climuni  11475  2clim  11483  climcn1  11490  climcn2  11491  subcn2  11493  mulcn2  11494  climsqz  11517  climsqz2  11518  climcau  11529  climcvg1nlem  11531  climcaucn  11533  serf0  11534  sumrbdclem  11559  summodclem2  11564  zsumdc  11566  divcnv  11679  absltap  11691  absgtap  11692  mertenslem2  11718  ntrivcvgap  11730  prodrbdclem  11753  prodmodclem2  11759  zproddc  11761  prodssdc  11771  fprodsplitdc  11778  fprodcl2lem  11787  efcllemp  11840  tanvalap  11890  sin01bnd  11939  cos01bnd  11940  sin01gt0  11944  absef  11952  eirrap  11960  dvds0  11988  dvdsmul1  11995  dvdsmultr1d  12014  dvdslelemd  12025  divconjdvds  12031  alzdvds  12036  3dvds  12046  sqoddm1div8z  12068  nno  12088  divalglemex  12104  bits0o  12132  dvdsbnd  12148  dvdslegcd  12156  zeqzmulgcd  12162  gcd0id  12171  gcdaddm  12176  gcd1  12179  gcdabs  12180  bezoutlemnewy  12188  bezoutlemstep  12189  bezoutlemmain  12190  bezoutlemex  12193  bezoutlemzz  12194  bezoutlemaz  12195  bezoutlembz  12196  bezoutlembi  12197  bezoutlemle  12200  bezoutlemsup  12201  mulgcd  12208  gcdzeq  12214  dvdsmulgcd  12217  sqgcd  12221  bezoutr1  12225  nninfctlemfo  12232  algcvga  12244  algfx  12245  eucalglt  12250  eucalg  12252  lcmneg  12267  lcmabs  12269  lcmgcdlem  12270  ncoprmgcdne1b  12282  mulgcddvds  12287  qredeq  12289  divgcdcoprm0  12294  cncongr1  12296  isprm2lem  12309  nprm  12316  dvdsnprmd  12318  prmdvdsfz  12332  isprm5lem  12334  coprm  12337  isprm6  12340  sqrt2irr  12355  pw2dvdslemn  12358  pw2dvdseulemle  12360  oddpwdclemdvds  12363  oddpwdclemndvds  12364  sqrt2irrap  12373  qnumdencl  12380  prmdiv  12428  modprmn0modprm0  12450  prm23lt5  12457  pythagtriplem4  12462  pythagtriplem19  12476  pythagtrip  12477  pclemub  12481  pcpre1  12486  pcpremul  12487  pceulem  12488  pcqcl  12500  pcidlem  12517  pcgcd1  12522  pc2dvds  12524  dvdsprmpweqle  12531  difsqpwdvds  12532  pcadd  12534  pcmpt  12537  expnprm  12547  pockthg  12551  infpnlem2  12554  prmunb  12556  1arith  12561  4sqlem10  12581  4sqlem11  12595  4sqlem12  12596  4sqlem13m  12597  4sqlem17  12601  4sqlem18  12602  ennnfonelemex  12656  ennnfonelemhom  12657  ennnfonelemrnh  12658  ennnfonelemnn0  12664  ennnfonelemim  12666  exmidunben  12668  ctinfomlemom  12669  ctinfom  12670  ctinf  12672  omctfn  12685  nninfdclemp1  12692  setscomd  12744  imasaddfnlemg  13016  mhmf1o  13172  grpinveu  13240  grpasscan1  13265  dfgrp3mlem  13300  grp1inv  13309  issubg4m  13399  ghmf1o  13481  srgisid  13618  ringadd2  13659  ringinvnzdiv  13682  unitgrp  13748  ringelnzr  13819  lringuplu  13828  subrguss  13868  subrgintm  13875  aprcotr  13917  islmodd  13925  lssclg  13996  lss0cl  14001  lssvneln0  14005  lss1d  14015  lmodindp1  14060  rnglidlmmgm  14128  znidomb  14290  znunit  14291  znrrg  14292  tgcl  14384  neii1  14467  neii2  14469  neiss  14470  tpnei  14480  tgrest  14489  ssrest  14502  icnpimaex  14531  lmcvg  14537  cnpnei  14539  cnptopco  14542  lmff  14569  txcnp  14591  txcn  14595  hmeontr  14633  blssec  14758  mopni3  14804  blsscls2  14813  comet  14819  bdxmet  14821  bdmopn  14824  xmettxlem  14829  xmettx  14830  addcncntoplem  14881  mpomulcn  14886  mulc1cncf  14909  cncfco  14911  cncfmptc  14916  mulcncflem  14927  mulcncf  14928  dedekindeulemlu  14941  dedekindeulemeu  14942  suplociccreex  14944  suplociccex  14945  dedekindicclemlu  14950  dedekindicclemeu  14951  ivthinclemlopn  14956  ivthinclemlr  14957  ivthinclemuopn  14958  ivthinclemur  14959  ivthinclemloc  14961  ivthinc  14963  ivthreinc  14965  ivthdichlem  14971  limcimolemlt  14984  limcresi  14986  cnplimcim  14987  cnplimclemle  14988  cnplimclemr  14989  limccnpcntop  14995  limccoap  14998  dvcoapbr  15027  dvcj  15029  plyf  15057  plyaddlem1  15067  plymullem1  15068  plyco  15079  plycj  15081  plycn  15082  plyrecj  15083  dvply2g  15086  efltlemlt  15094  sin0pilem2  15102  tangtx  15158  logdivlti  15201  rplogbval  15265  logbgcd1irraplemexp  15288  logbgcd1irraplemap  15289  logbgcd1irrap  15290  perfect1  15318  perfectlem1  15319  perfectlem2  15320  lgsval4a  15347  lgsdir2lem3  15355  lgsne0  15363  gausslemma2dlem3  15388  gausslemma2dlem4  15389  gausslemma2dlem6  15392  gausslemma2dlem7  15393  gausslemma2d  15394  lgseisenlem1  15395  lgsquadlem2  15403  lgsquadlem3  15404  lgsquad2lem2  15407  lgsquad3  15409  2lgsoddprmlem2  15431  2sqlem8a  15447  2sqlem8  15448  2sqlem9  15449  bj-exlimmpi  15500  uzdcinzz  15528  bj-charfundcALT  15539  bj-2inf  15668  bj-peano4  15685  bj-nn0suc  15694  1dom1el  15721  subctctexmid  15731  nninfalllem1  15739  nninfsellemqall  15746  nninfomnilem  15749  nninffeq  15751  exmidsbthrlem  15753  sbthomlem  15756  refeq  15759  isomninnlem  15761  apdifflemr  15778  redcwlpo  15786  reap0  15789  nconstwlpolem  15796