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  1352  xor3dc  1406  exlimdd  1894  exlimddv  1921  eqrdav  2203  necon1aidc  2426  necon1bidc  2427  necon4aidc  2443  reximddv  2608  reximssdv  2609  rexlimddv  2627  vtoclgft  2822  rspcedvd  2882  sseldd  3193  ssneldd  3195  tpid3g  3747  preq12b  3810  axpweq  4214  exmid1dc  4243  exmid1stab  4251  opth  4280  issod  4365  frirrg  4396  frind  4398  ralxfr2d  4510  rexxfr2d  4511  eldifpw  4523  onun2  4537  onuni  4541  elirr  4588  en2lp  4601  wetriext  4624  peano2  4642  relop  4827  elres  4994  sotri2  5079  iota4an  5251  iota5  5252  funeu  5295  funopg  5304  imadiflem  5352  funimaexglem  5356  ssimaex  5639  ffvelcdm  5712  dff3im  5724  dffo4  5727  funopsn  5761  f1eqcocnv  5859  f1oiso2  5895  riota5f  5923  riotass2  5925  acexmidlemcase  5938  ovmpodf  6076  ovmpodv2  6078  ovi3  6082  ov6g  6083  caoftrn  6190  op1steq  6264  tfr0dm  6407  tfrlemibxssdm  6412  tfrlemi14d  6418  tfr1onlembxssdm  6428  tfr1onlemaccex  6433  tfr1onlemres  6434  tfrcllembxssdm  6441  tfrcllemaccex  6446  tfrcllemres  6447  rdgivallem  6466  nnsucelsuc  6576  nnsucsssuc  6577  dcdifsnid  6589  nnawordex  6614  ersym  6631  mapvalg  6744  pmvalg  6745  mapsn  6776  fundmen  6897  en2  6911  pw2f1odclem  6930  mapdom1g  6943  fidceq  6965  fin0or  6982  findcard2  6985  findcard2s  6986  prfidceq  7024  fiintim  7027  suplub2ti  7102  supsnti  7106  supisoex  7110  difinfsnlem  7200  difinfsn  7201  ctm  7210  ctssdclemn0  7211  ctssdccl  7212  ctssdc  7214  enumctlemm  7215  nninfninc  7224  nnnninfeq2  7230  enomnilem  7239  exmidomniim  7242  exmidomni  7243  fodjuomnilemdc  7245  fodjuomnilemres  7249  omnimkv  7257  mkvprop  7259  omniwomnimkv  7268  en2eleq  7302  acfun  7318  exmidontriimlem1  7332  exmidontriimlem4  7335  exmidontriim  7336  ccfunen  7375  cc4f  7380  cc4n  7382  elni2  7426  mulclpi  7440  nlt1pig  7453  indpi  7454  recclnq  7504  ltexnqq  7520  halfnqq  7522  prarloclemarch  7530  prarloclemarch2  7531  prop  7587  prltlu  7599  prarloclem3step  7608  prarloclem5  7612  prarloclem  7613  prarloc  7615  prarloc2  7616  genpml  7629  genpmu  7630  genprndl  7633  genprndu  7634  genpdisj  7635  addnqprllem  7639  addnqprulem  7640  addlocprlemeq  7645  addlocprlemgt  7646  addlocprlem  7647  addlocpr  7648  nqprloc  7657  nqprl  7663  nqpru  7664  addnqprlemrl  7669  addnqprlemru  7670  appdivnq  7675  prmuloc  7678  prmuloc2  7679  mullocprlem  7682  mullocpr  7683  mulnqprlemrl  7685  mulnqprlemru  7686  ltprordil  7701  ltpopr  7707  ltsopr  7708  ltaddpr  7709  ltexprlemm  7712  ltexprlemopl  7713  ltexprlemlol  7714  ltexprlemopu  7715  ltexprlemupu  7716  ltexprlemloc  7719  ltexprlemfl  7721  ltexprlemrl  7722  ltexprlemfu  7723  ltexprlemru  7724  ltaprg  7731  recexprlemm  7736  recexprlem1ssl  7745  recexprlem1ssu  7746  aptiprleml  7751  aptiprlemu  7752  archpr  7755  cauappcvgprlemm  7757  cauappcvgprlemopl  7758  cauappcvgprlemlol  7759  cauappcvgprlemopu  7760  cauappcvgprlemupu  7761  cauappcvgprlemdisj  7763  cauappcvgprlemloc  7764  cauappcvgprlemladdfu  7766  cauappcvgprlemladdfl  7767  cauappcvgprlemladdru  7768  cauappcvgprlem1  7771  archrecpr  7776  caucvgprlemnkj  7778  caucvgprlemnbj  7779  caucvgprlemm  7780  caucvgprlemopl  7781  caucvgprlemlol  7782  caucvgprlemopu  7783  caucvgprlemupu  7784  caucvgprlemdisj  7786  caucvgprlemloc  7787  caucvgprlemladdfu  7789  caucvgprlem1  7791  caucvgprlemlim  7793  caucvgprprlemnbj  7805  caucvgprprlemml  7806  caucvgprprlemopl  7809  caucvgprprlemlol  7810  caucvgprprlemopu  7811  caucvgprprlemupu  7812  caucvgprprlemdisj  7814  caucvgprprlemloc  7815  caucvgprprlemexbt  7818  caucvgprprlemaddq  7820  caucvgprprlemlim  7823  suplocexprlemss  7827  suplocexprlemrl  7829  suplocexprlemmu  7830  suplocexprlemru  7831  suplocexprlemdisj  7832  suplocexprlemloc  7833  suplocexprlemub  7835  suplocexprlemlub  7836  recexgt0sr  7885  mulgt0sr  7890  archsr  7894  caucvgsrlemoffcau  7910  suplocsrlemb  7918  suplocsrlempr  7919  suplocsrlem  7920  cnm  7944  axarch  8003  axcaucvglemcau  8010  axpre-suploclemres  8013  lelttr  8160  ltletr  8161  ltled  8190  cnegexlem1  8246  cnegexlem2  8247  renegcl  8332  negf1o  8453  gt0add  8645  apreap  8659  apirr  8677  apsym  8678  apcotr  8679  apadd1  8680  apneg  8683  mulext1  8684  mulap0r  8687  apti  8694  aprcl  8718  aptap  8722  recexap  8725  mulap0  8726  receuap  8741  mul0eqap  8742  lep1  8917  lem1  8919  letrp1  8920  recreclt  8972  lbinf  9020  suprubex  9023  nnrecgt0  9073  bndndx  9293  nn0ge2m1nn  9354  elnn0z  9384  peano2z  9407  zaddcl  9411  ztri3or0  9413  zltnle  9417  zdceq  9447  zdcle  9448  zdclt  9449  zdiv  9460  zeo  9477  fnn0ind  9488  btwnz  9491  uzm1  9678  uzp1  9681  indstr  9713  supinfneg  9715  infsupneg  9716  eluzdc  9730  nn01to3  9737  qapne  9759  xrltled  9920  xrlelttr  9927  xrltletr  9928  ge0nemnf  9945  fzdcel  10161  elfzouz2  10283  fzoss1  10293  fzospliti  10298  elincfzoext  10320  fzocatel  10326  fzostep1  10364  zsupcllemstep  10370  zsupcl  10372  infssuzledc  10375  qtri3or  10381  qltnle  10384  qdceq  10385  qdclt  10386  exbtwnzlemex  10390  rebtwn2zlemstep  10393  rebtwn2z  10395  qbtwnxr  10398  ioom  10401  ico0  10402  ioc0  10403  flqeqceilz  10461  modqadd1  10504  modqmul1  10520  frec2uzuzd  10545  frec2uzlt2d  10547  frec2uzf1od  10549  frecuzrdgrrn  10551  frec2uzrdg  10552  frecuzrdgrcl  10553  frecuzrdgsuc  10557  frecuzrdgrclt  10558  frecuzrdgdomlem  10560  uzsinds  10587  seqvalcd  10604  seqovcd  10610  seq3fveq2  10618  seqfveq2g  10620  seq3shft2  10624  seqshft2g  10625  monoord  10628  seq3split  10631  seqsplitg  10632  seq3caopr3  10634  iseqf1olemab  10645  iseqf1olemnanb  10646  iseqf1olemqk  10650  seqf1oglem1  10662  seqf1og  10664  seq3id3  10667  seq3id2  10669  seq3homo  10670  seqhomog  10673  expgt1  10720  m1expeven  10729  expnbnd  10806  expnlbnd2  10808  nn0ltexp2  10852  apexp1  10861  hashennn  10923  zfz1isolem1  10983  seq3coll  10985  cjap  11188  caucvgre  11263  cvg1nlemres  11267  resqrexlemgt0  11302  resqrexlemglsq  11304  resqrexlemga  11305  resqrtcl  11311  abslt  11370  abssubap0  11372  abssubne0  11373  caubnd2  11399  qdenre  11484  maxabslemlub  11489  maxabs  11491  maxleast  11495  fimaxre2  11509  xrmaxiflemlub  11530  xrmaxif  11533  xrmaxltsup  11540  xrmaxadd  11543  xrmineqinf  11551  climuni  11575  2clim  11583  climcn1  11590  climcn2  11591  subcn2  11593  mulcn2  11594  climsqz  11617  climsqz2  11618  climcau  11629  climcvg1nlem  11631  climcaucn  11633  serf0  11634  sumrbdclem  11659  summodclem2  11664  zsumdc  11666  divcnv  11779  absltap  11791  absgtap  11792  mertenslem2  11818  ntrivcvgap  11830  prodrbdclem  11853  prodmodclem2  11859  zproddc  11861  prodssdc  11871  fprodsplitdc  11878  fprodcl2lem  11887  efcllemp  11940  tanvalap  11990  sin01bnd  12039  cos01bnd  12040  sin01gt0  12044  absef  12052  eirrap  12060  dvds0  12088  dvdsmul1  12095  dvdsmultr1d  12114  dvdslelemd  12125  divconjdvds  12131  alzdvds  12136  3dvds  12146  sqoddm1div8z  12168  nno  12188  divalglemex  12204  bits0o  12232  dvdsbnd  12248  dvdslegcd  12256  zeqzmulgcd  12262  gcd0id  12271  gcdaddm  12276  gcd1  12279  gcdabs  12280  bezoutlemnewy  12288  bezoutlemstep  12289  bezoutlemmain  12290  bezoutlemex  12293  bezoutlemzz  12294  bezoutlemaz  12295  bezoutlembz  12296  bezoutlembi  12297  bezoutlemle  12300  bezoutlemsup  12301  mulgcd  12308  gcdzeq  12314  dvdsmulgcd  12317  sqgcd  12321  bezoutr1  12325  nninfctlemfo  12332  algcvga  12344  algfx  12345  eucalglt  12350  eucalg  12352  lcmneg  12367  lcmabs  12369  lcmgcdlem  12370  ncoprmgcdne1b  12382  mulgcddvds  12387  qredeq  12389  divgcdcoprm0  12394  cncongr1  12396  isprm2lem  12409  nprm  12416  dvdsnprmd  12418  prmdvdsfz  12432  isprm5lem  12434  coprm  12437  isprm6  12440  sqrt2irr  12455  pw2dvdslemn  12458  pw2dvdseulemle  12460  oddpwdclemdvds  12463  oddpwdclemndvds  12464  sqrt2irrap  12473  qnumdencl  12480  prmdiv  12528  modprmn0modprm0  12550  prm23lt5  12557  pythagtriplem4  12562  pythagtriplem19  12576  pythagtrip  12577  pclemub  12581  pcpre1  12586  pcpremul  12587  pceulem  12588  pcqcl  12600  pcidlem  12617  pcgcd1  12622  pc2dvds  12624  dvdsprmpweqle  12631  difsqpwdvds  12632  pcadd  12634  pcmpt  12637  expnprm  12647  pockthg  12651  infpnlem2  12654  prmunb  12656  1arith  12661  4sqlem10  12681  4sqlem11  12695  4sqlem12  12696  4sqlem13m  12697  4sqlem17  12701  4sqlem18  12702  ennnfonelemex  12756  ennnfonelemhom  12757  ennnfonelemrnh  12758  ennnfonelemnn0  12764  ennnfonelemim  12766  exmidunben  12768  ctinfomlemom  12769  ctinfom  12770  ctinf  12772  omctfn  12785  nninfdclemp1  12792  setscomd  12844  imasaddfnlemg  13117  mhmf1o  13273  grpinveu  13341  grpasscan1  13366  dfgrp3mlem  13401  grp1inv  13410  issubg4m  13500  ghmf1o  13582  srgisid  13719  ringadd2  13760  ringinvnzdiv  13783  unitgrp  13849  ringelnzr  13920  lringuplu  13929  subrguss  13969  subrgintm  13976  aprcotr  14018  islmodd  14026  lssclg  14097  lss0cl  14102  lssvneln0  14106  lss1d  14116  lmodindp1  14161  rnglidlmmgm  14229  znidomb  14391  znunit  14392  znrrg  14393  mplsubgfilemcl  14432  mplsubgfileminv  14433  tgcl  14507  neii1  14590  neii2  14592  neiss  14593  tpnei  14603  tgrest  14612  ssrest  14625  icnpimaex  14654  lmcvg  14660  cnpnei  14662  cnptopco  14665  lmff  14692  txcnp  14714  txcn  14718  hmeontr  14756  blssec  14881  mopni3  14927  blsscls2  14936  comet  14942  bdxmet  14944  bdmopn  14947  xmettxlem  14952  xmettx  14953  addcncntoplem  15004  mpomulcn  15009  mulc1cncf  15032  cncfco  15034  cncfmptc  15039  mulcncflem  15050  mulcncf  15051  dedekindeulemlu  15064  dedekindeulemeu  15065  suplociccreex  15067  suplociccex  15068  dedekindicclemlu  15073  dedekindicclemeu  15074  ivthinclemlopn  15079  ivthinclemlr  15080  ivthinclemuopn  15081  ivthinclemur  15082  ivthinclemloc  15084  ivthinc  15086  ivthreinc  15088  ivthdichlem  15094  limcimolemlt  15107  limcresi  15109  cnplimcim  15110  cnplimclemle  15111  cnplimclemr  15112  limccnpcntop  15118  limccoap  15121  dvcoapbr  15150  dvcj  15152  plyf  15180  plyaddlem1  15190  plymullem1  15191  plyco  15202  plycj  15204  plycn  15205  plyrecj  15206  dvply2g  15209  efltlemlt  15217  sin0pilem2  15225  tangtx  15281  logdivlti  15324  rplogbval  15388  logbgcd1irraplemexp  15411  logbgcd1irraplemap  15412  logbgcd1irrap  15413  perfect1  15441  perfectlem1  15442  perfectlem2  15443  lgsval4a  15470  lgsdir2lem3  15478  lgsne0  15486  gausslemma2dlem3  15511  gausslemma2dlem4  15512  gausslemma2dlem6  15515  gausslemma2dlem7  15516  gausslemma2d  15517  lgseisenlem1  15518  lgsquadlem2  15526  lgsquadlem3  15527  lgsquad2lem2  15530  lgsquad3  15532  2lgsoddprmlem2  15554  2sqlem8a  15570  2sqlem8  15571  2sqlem9  15572  bj-exlimmpi  15668  uzdcinzz  15696  bj-charfundcALT  15707  bj-2inf  15836  bj-peano4  15853  bj-nn0suc  15862  1dom1el  15889  subctctexmid  15899  nninfalllem1  15907  nninfsellemqall  15914  nninfomnilem  15917  nninffeq  15919  nnnninfex  15921  exmidsbthrlem  15923  sbthomlem  15926  refeq  15929  isomninnlem  15931  apdifflemr  15948  redcwlpo  15956  reap0  15959  nconstwlpolem  15966