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  11159  caucvgre  11234  cvg1nlemres  11238  resqrexlemgt0  11273  resqrexlemglsq  11275  resqrexlemga  11276  resqrtcl  11282  abslt  11341  abssubap0  11343  abssubne0  11344  caubnd2  11370  qdenre  11455  maxabslemlub  11460  maxabs  11462  maxleast  11466  fimaxre2  11480  xrmaxiflemlub  11501  xrmaxif  11504  xrmaxltsup  11511  xrmaxadd  11514  xrmineqinf  11522  climuni  11546  2clim  11554  climcn1  11561  climcn2  11562  subcn2  11564  mulcn2  11565  climsqz  11588  climsqz2  11589  climcau  11600  climcvg1nlem  11602  climcaucn  11604  serf0  11605  sumrbdclem  11630  summodclem2  11635  zsumdc  11637  divcnv  11750  absltap  11762  absgtap  11763  mertenslem2  11789  ntrivcvgap  11801  prodrbdclem  11824  prodmodclem2  11830  zproddc  11832  prodssdc  11842  fprodsplitdc  11849  fprodcl2lem  11858  efcllemp  11911  tanvalap  11961  sin01bnd  12010  cos01bnd  12011  sin01gt0  12015  absef  12023  eirrap  12031  dvds0  12059  dvdsmul1  12066  dvdsmultr1d  12085  dvdslelemd  12096  divconjdvds  12102  alzdvds  12107  3dvds  12117  sqoddm1div8z  12139  nno  12159  divalglemex  12175  bits0o  12203  dvdsbnd  12219  dvdslegcd  12227  zeqzmulgcd  12233  gcd0id  12242  gcdaddm  12247  gcd1  12250  gcdabs  12251  bezoutlemnewy  12259  bezoutlemstep  12260  bezoutlemmain  12261  bezoutlemex  12264  bezoutlemzz  12265  bezoutlemaz  12266  bezoutlembz  12267  bezoutlembi  12268  bezoutlemle  12271  bezoutlemsup  12272  mulgcd  12279  gcdzeq  12285  dvdsmulgcd  12288  sqgcd  12292  bezoutr1  12296  nninfctlemfo  12303  algcvga  12315  algfx  12316  eucalglt  12321  eucalg  12323  lcmneg  12338  lcmabs  12340  lcmgcdlem  12341  ncoprmgcdne1b  12353  mulgcddvds  12358  qredeq  12360  divgcdcoprm0  12365  cncongr1  12367  isprm2lem  12380  nprm  12387  dvdsnprmd  12389  prmdvdsfz  12403  isprm5lem  12405  coprm  12408  isprm6  12411  sqrt2irr  12426  pw2dvdslemn  12429  pw2dvdseulemle  12431  oddpwdclemdvds  12434  oddpwdclemndvds  12435  sqrt2irrap  12444  qnumdencl  12451  prmdiv  12499  modprmn0modprm0  12521  prm23lt5  12528  pythagtriplem4  12533  pythagtriplem19  12547  pythagtrip  12548  pclemub  12552  pcpre1  12557  pcpremul  12558  pceulem  12559  pcqcl  12571  pcidlem  12588  pcgcd1  12593  pc2dvds  12595  dvdsprmpweqle  12602  difsqpwdvds  12603  pcadd  12605  pcmpt  12608  expnprm  12618  pockthg  12622  infpnlem2  12625  prmunb  12627  1arith  12632  4sqlem10  12652  4sqlem11  12666  4sqlem12  12667  4sqlem13m  12668  4sqlem17  12672  4sqlem18  12673  ennnfonelemex  12727  ennnfonelemhom  12728  ennnfonelemrnh  12729  ennnfonelemnn0  12735  ennnfonelemim  12737  exmidunben  12739  ctinfomlemom  12740  ctinfom  12741  ctinf  12743  omctfn  12756  nninfdclemp1  12763  setscomd  12815  imasaddfnlemg  13088  mhmf1o  13244  grpinveu  13312  grpasscan1  13337  dfgrp3mlem  13372  grp1inv  13381  issubg4m  13471  ghmf1o  13553  srgisid  13690  ringadd2  13731  ringinvnzdiv  13754  unitgrp  13820  ringelnzr  13891  lringuplu  13900  subrguss  13940  subrgintm  13947  aprcotr  13989  islmodd  13997  lssclg  14068  lss0cl  14073  lssvneln0  14077  lss1d  14087  lmodindp1  14132  rnglidlmmgm  14200  znidomb  14362  znunit  14363  znrrg  14364  mplsubgfilemcl  14403  mplsubgfileminv  14404  tgcl  14478  neii1  14561  neii2  14563  neiss  14564  tpnei  14574  tgrest  14583  ssrest  14596  icnpimaex  14625  lmcvg  14631  cnpnei  14633  cnptopco  14636  lmff  14663  txcnp  14685  txcn  14689  hmeontr  14727  blssec  14852  mopni3  14898  blsscls2  14907  comet  14913  bdxmet  14915  bdmopn  14918  xmettxlem  14923  xmettx  14924  addcncntoplem  14975  mpomulcn  14980  mulc1cncf  15003  cncfco  15005  cncfmptc  15010  mulcncflem  15021  mulcncf  15022  dedekindeulemlu  15035  dedekindeulemeu  15036  suplociccreex  15038  suplociccex  15039  dedekindicclemlu  15044  dedekindicclemeu  15045  ivthinclemlopn  15050  ivthinclemlr  15051  ivthinclemuopn  15052  ivthinclemur  15053  ivthinclemloc  15055  ivthinc  15057  ivthreinc  15059  ivthdichlem  15065  limcimolemlt  15078  limcresi  15080  cnplimcim  15081  cnplimclemle  15082  cnplimclemr  15083  limccnpcntop  15089  limccoap  15092  dvcoapbr  15121  dvcj  15123  plyf  15151  plyaddlem1  15161  plymullem1  15162  plyco  15173  plycj  15175  plycn  15176  plyrecj  15177  dvply2g  15180  efltlemlt  15188  sin0pilem2  15196  tangtx  15252  logdivlti  15295  rplogbval  15359  logbgcd1irraplemexp  15382  logbgcd1irraplemap  15383  logbgcd1irrap  15384  perfect1  15412  perfectlem1  15413  perfectlem2  15414  lgsval4a  15441  lgsdir2lem3  15449  lgsne0  15457  gausslemma2dlem3  15482  gausslemma2dlem4  15483  gausslemma2dlem6  15486  gausslemma2dlem7  15487  gausslemma2d  15488  lgseisenlem1  15489  lgsquadlem2  15497  lgsquadlem3  15498  lgsquad2lem2  15501  lgsquad3  15503  2lgsoddprmlem2  15525  2sqlem8a  15541  2sqlem8  15542  2sqlem9  15543  bj-exlimmpi  15639  uzdcinzz  15667  bj-charfundcALT  15678  bj-2inf  15807  bj-peano4  15824  bj-nn0suc  15833  1dom1el  15860  subctctexmid  15870  nninfalllem1  15878  nninfsellemqall  15885  nninfomnilem  15888  nninffeq  15890  nnnninfex  15892  exmidsbthrlem  15894  sbthomlem  15897  refeq  15900  isomninnlem  15902  apdifflemr  15919  redcwlpo  15927  reap0  15930  nconstwlpolem  15937