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  625  mt2d  630  mpnanrd  700  mpjaod  726  stdcndcOLD  854  impidc  866  jadc  871  pm2.54dc  899  oplem1  984  mp3and  1377  xor3dc  1432  exlimdd  1921  exlimddv  1948  eqrdav  2231  necon1aidc  2463  necon1bidc  2464  necon4aidc  2480  reximddv  2645  reximssdv  2646  rexlimddv  2665  vtoclgft  2865  rspcedvd  2927  sseldd  3239  ssneldd  3241  tpid3g  3807  preq12b  3874  axpweq  4284  exmid1dc  4313  exmid1stab  4321  opth  4353  issod  4440  frirrg  4471  frind  4473  ralxfr2d  4585  rexxfr2d  4586  eldifpw  4598  onun2  4612  onuni  4616  elirr  4663  en2lp  4676  wetriext  4699  peano2  4717  relop  4905  elres  5074  sotri2  5160  iota4an  5333  iota5  5334  funeu  5377  funopg  5386  imadiflem  5435  funimaexglem  5439  ssimaex  5738  ffvelcdm  5810  dff3im  5822  dffo4  5825  funopsn  5860  f1eqcocnv  5964  f1oiso2  6000  riota5f  6030  riotass2  6032  acexmidlemcase  6045  elovimad  6094  ovmpodf  6185  ovmpodv2  6187  ovi3  6191  ov6g  6192  caoftrn  6299  op1steq  6373  fvdifsuppst  6444  suppssdc  6460  suppofss1dcl  6464  suppofss2dcl  6465  tfr0dm  6553  tfrlemibxssdm  6558  tfrlemi14d  6564  tfr1onlembxssdm  6574  tfr1onlemaccex  6579  tfr1onlemres  6580  tfrcllembxssdm  6587  tfrcllemaccex  6592  tfrcllemres  6593  rdgivallem  6612  nnsucelsuc  6724  nnsucsssuc  6725  dcdifsnid  6737  nnawordex  6762  ersym  6779  mapvalg  6892  pmvalg  6893  mapsnd  6923  mapsn  6925  fundmen  7047  1dom1el  7060  en2  7065  pw2f1odclem  7087  mapdom1g  7100  fidceq  7124  fin0or  7143  findcard2  7146  findcard2s  7147  fidcen  7156  prfidceq  7188  fiintim  7191  suplub2ti  7292  supsnti  7296  supisoex  7300  difinfsnlem  7390  difinfsn  7391  ctm  7400  ctssdclemn0  7401  ctssdccl  7402  ctssdc  7404  enumctlemm  7405  nninfninc  7414  nnnninfeq2  7420  enomnilem  7429  exmidomniim  7432  exmidomni  7433  fodjuomnilemdc  7435  fodjuomnilemres  7439  omnimkv  7447  mkvprop  7449  omniwomnimkv  7458  en2prde  7490  pr2cv1  7492  en2eleq  7498  acfun  7514  exmidontriimlem1  7528  exmidontriimlem4  7531  exmidontriim  7532  papsym  7561  papcotr  7562  ccfunen  7578  cc4f  7583  cc4n  7585  elni2  7629  mulclpi  7643  nlt1pig  7656  indpi  7657  recclnq  7707  ltexnqq  7723  halfnqq  7725  prarloclemarch  7733  prarloclemarch2  7734  prop  7790  prltlu  7802  prarloclem3step  7811  prarloclem5  7815  prarloclem  7816  prarloc  7818  prarloc2  7819  genpml  7832  genpmu  7833  genprndl  7836  genprndu  7837  genpdisj  7838  addnqprllem  7842  addnqprulem  7843  addlocprlemeq  7848  addlocprlemgt  7849  addlocprlem  7850  addlocpr  7851  nqprloc  7860  nqprl  7866  nqpru  7867  addnqprlemrl  7872  addnqprlemru  7873  appdivnq  7878  prmuloc  7881  prmuloc2  7882  mullocprlem  7885  mullocpr  7886  mulnqprlemrl  7888  mulnqprlemru  7889  ltprordil  7904  ltpopr  7910  ltsopr  7911  ltaddpr  7912  ltexprlemm  7915  ltexprlemopl  7916  ltexprlemlol  7917  ltexprlemopu  7918  ltexprlemupu  7919  ltexprlemloc  7922  ltexprlemfl  7924  ltexprlemrl  7925  ltexprlemfu  7926  ltexprlemru  7927  ltaprg  7934  recexprlemm  7939  recexprlem1ssl  7948  recexprlem1ssu  7949  aptiprleml  7954  aptiprlemu  7955  archpr  7958  cauappcvgprlemm  7960  cauappcvgprlemopl  7961  cauappcvgprlemlol  7962  cauappcvgprlemopu  7963  cauappcvgprlemupu  7964  cauappcvgprlemdisj  7966  cauappcvgprlemloc  7967  cauappcvgprlemladdfu  7969  cauappcvgprlemladdfl  7970  cauappcvgprlemladdru  7971  cauappcvgprlem1  7974  archrecpr  7979  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprlemm  7983  caucvgprlemopl  7984  caucvgprlemlol  7985  caucvgprlemopu  7986  caucvgprlemupu  7987  caucvgprlemdisj  7989  caucvgprlemloc  7990  caucvgprlemladdfu  7992  caucvgprlem1  7994  caucvgprlemlim  7996  caucvgprprlemnbj  8008  caucvgprprlemml  8009  caucvgprprlemopl  8012  caucvgprprlemlol  8013  caucvgprprlemopu  8014  caucvgprprlemupu  8015  caucvgprprlemdisj  8017  caucvgprprlemloc  8018  caucvgprprlemexbt  8021  caucvgprprlemaddq  8023  caucvgprprlemlim  8026  suplocexprlemss  8030  suplocexprlemrl  8032  suplocexprlemmu  8033  suplocexprlemru  8034  suplocexprlemdisj  8035  suplocexprlemloc  8036  suplocexprlemub  8038  suplocexprlemlub  8039  recexgt0sr  8088  mulgt0sr  8093  archsr  8097  caucvgsrlemoffcau  8113  suplocsrlemb  8121  suplocsrlempr  8122  suplocsrlem  8123  cnm  8147  axarch  8206  axcaucvglemcau  8213  axpre-suploclemres  8216  lelttr  8362  ltletr  8363  ltled  8392  cnegexlem1  8448  cnegexlem2  8449  renegcl  8534  negf1o  8655  gt0add  8847  apreap  8861  apirr  8879  apsym  8880  apcotr  8881  apadd1  8882  apneg  8885  mulext1  8886  mulap0r  8889  apti  8896  aprcl  8920  aptap  8924  recexap  8927  mulap0  8928  receuap  8943  mul0eqap  8944  lep1  9119  lem1  9121  letrp1  9122  recreclt  9174  lbinf  9222  suprubex  9225  nnrecgt0  9275  bndndx  9495  nn0ge2m1nn  9560  elnn0z  9590  peano2z  9613  zaddcl  9617  ztri3or0  9619  zltnle  9623  zdceq  9653  zdcle  9654  zdclt  9655  zdiv  9666  zeo  9683  fnn0ind  9694  btwnz  9697  uzm1  9885  uzp1  9888  indstr  9925  supinfneg  9927  infsupneg  9928  eluzdc  9942  nn01to3  9949  qapne  9971  xrltled  10132  xrlelttr  10139  xrltletr  10140  ge0nemnf  10157  fzdcel  10374  elfzouz2  10496  fzoss1  10507  fzospliti  10512  elincfzoext  10538  fzocatel  10544  fzostep1  10583  zsupcllemstep  10589  zsupcl  10591  infssuzledc  10594  qtri3or  10600  qltnle  10603  qdceq  10604  qdclt  10605  exbtwnzlemex  10609  rebtwn2zlemstep  10612  rebtwn2z  10614  qbtwnxr  10617  ioom  10620  ico0  10621  ioc0  10622  flqeqceilz  10680  modqadd1  10723  modqmul1  10739  frec2uzuzd  10764  frec2uzlt2d  10766  frec2uzf1od  10768  frecuzrdgrrn  10770  frec2uzrdg  10771  frecuzrdgrcl  10772  frecuzrdgsuc  10776  frecuzrdgrclt  10777  frecuzrdgdomlem  10779  uzsinds  10806  seqvalcd  10823  seqovcd  10829  seq3fveq2  10837  seqfveq2g  10839  seq3shft2  10843  seqshft2g  10844  monoord  10847  seq3split  10850  seqsplitg  10851  seq3caopr3  10853  iseqf1olemab  10864  iseqf1olemnanb  10865  iseqf1olemqk  10869  seqf1oglem1  10881  seqf1og  10883  seq3id3  10886  seq3id2  10888  seq3homo  10889  seqhomog  10892  expgt1  10939  m1expeven  10948  expnbnd  11025  expnlbnd2  11027  nn0ltexp2  11071  apexp1  11080  hashennn  11143  hashfibclem  11206  zfz1isolem1  11212  seq3coll  11214  pfxwrdsymbg  11382  wrdind  11414  wrd2ind  11415  cjap  11591  caucvgre  11666  cvg1nlemres  11670  resqrexlemgt0  11705  resqrexlemglsq  11707  resqrexlemga  11708  resqrtcl  11714  abslt  11773  abssubap0  11775  abssubne0  11776  caubnd2  11802  qdenre  11887  maxabslemlub  11892  maxabs  11894  maxleast  11898  fimaxre2  11912  xrmaxiflemlub  11933  xrmaxif  11936  xrmaxltsup  11943  xrmaxadd  11946  xrmineqinf  11954  climuni  11978  2clim  11986  climcn1  11993  climcn2  11994  subcn2  11996  mulcn2  11997  climsqz  12020  climsqz2  12021  climcau  12032  climcvg1nlem  12034  climcaucn  12036  serf0  12037  sumrbdclem  12063  summodclem2  12068  zsumdc  12070  divcnv  12183  absltap  12195  absgtap  12196  mertenslem2  12222  ntrivcvgap  12234  prodrbdclem  12257  prodmodclem2  12263  zproddc  12265  prodssdc  12275  fprodsplitdc  12282  fprodcl2lem  12291  efcllemp  12344  tanvalap  12394  sin01bnd  12443  cos01bnd  12444  sin01gt0  12448  absef  12456  eirrap  12464  dvds0  12492  dvdsmul1  12499  dvdsmultr1d  12518  dvdslelemd  12529  divconjdvds  12535  alzdvds  12540  3dvds  12550  sqoddm1div8z  12572  nno  12592  divalglemex  12608  bits0o  12636  dvdsbnd  12652  dvdslegcd  12660  zeqzmulgcd  12666  gcd0id  12675  gcdaddm  12680  gcd1  12683  gcdabs  12684  bezoutlemnewy  12692  bezoutlemstep  12693  bezoutlemmain  12694  bezoutlemex  12697  bezoutlemzz  12698  bezoutlemaz  12699  bezoutlembz  12700  bezoutlembi  12701  bezoutlemle  12704  bezoutlemsup  12705  mulgcd  12712  gcdzeq  12718  dvdsmulgcd  12721  sqgcd  12725  bezoutr1  12729  nninfctlemfo  12736  algcvga  12748  algfx  12749  eucalglt  12754  eucalg  12756  lcmneg  12771  lcmabs  12773  lcmgcdlem  12774  ncoprmgcdne1b  12786  mulgcddvds  12791  qredeq  12793  divgcdcoprm0  12798  cncongr1  12800  isprm2lem  12813  nprm  12820  dvdsnprmd  12822  prmdvdsfz  12836  isprm5lem  12838  coprm  12841  isprm6  12844  sqrt2irr  12859  pw2dvdslemn  12862  pw2dvdseulemle  12864  oddpwdclemdvds  12867  oddpwdclemndvds  12868  sqrt2irrap  12877  qnumdencl  12884  prmdiv  12932  modprmn0modprm0  12954  prm23lt5  12961  pythagtriplem4  12966  pythagtriplem19  12980  pythagtrip  12981  pclemub  12985  pcpre1  12990  pcpremul  12991  pceulem  12992  pcqcl  13004  pcidlem  13021  pcgcd1  13026  pc2dvds  13028  dvdsprmpweqle  13035  difsqpwdvds  13036  pcadd  13038  pcmpt  13041  expnprm  13051  pockthg  13055  infpnlem2  13058  prmunb  13060  1arith  13065  4sqlem10  13085  4sqlem11  13099  4sqlem12  13100  4sqlem13m  13101  4sqlem17  13105  4sqlem18  13106  ennnfonelemex  13165  ennnfonelemhom  13166  ennnfonelemrnh  13167  ennnfonelemnn0  13173  ennnfonelemim  13175  exmidunben  13177  ctinfomlemom  13178  ctinfom  13179  ctinf  13181  omctfn  13194  nninfdclemp1  13201  setscomd  13253  imasaddfnlemg  13527  mhmf1o  13683  grpinveu  13751  grpasscan1  13776  dfgrp3mlem  13811  grp1inv  13820  issubg4m  13910  ghmf1o  13992  srgisid  14130  ringadd2  14171  ringinvnzdiv  14194  unitgrp  14261  ringelnzr  14332  lringuplu  14341  subrguss  14381  subrgintm  14388  aprcotr  14431  islmodd  14441  lssclg  14512  lss0cl  14517  lssvneln0  14521  lss1d  14531  lmodindp1  14576  rnglidlmmgm  14644  znidomb  14806  znunit  14807  znrrg  14808  mplsubgfilemcl  14854  mplsubgfileminv  14855  tgcl  14929  neii1  15012  neii2  15014  neiss  15015  tpnei  15025  tgrest  15034  ssrest  15047  icnpimaex  15076  lmcvg  15082  cnpnei  15084  cnptopco  15087  lmff  15114  txcnp  15136  txcn  15140  hmeontr  15178  blssec  15303  mopni3  15349  blsscls2  15358  comet  15364  bdxmet  15366  bdmopn  15369  xmettxlem  15374  xmettx  15375  addcncntoplem  15426  mpomulcn  15431  mulc1cncf  15454  cncfco  15456  cncfmptc  15461  mulcncflem  15472  mulcncf  15473  dedekindeulemlu  15486  dedekindeulemeu  15487  suplociccreex  15489  suplociccex  15490  dedekindicclemlu  15495  dedekindicclemeu  15496  ivthinclemlopn  15501  ivthinclemlr  15502  ivthinclemuopn  15503  ivthinclemur  15504  ivthinclemloc  15506  ivthinc  15508  ivthreinc  15510  ivthdichlem  15516  limcimolemlt  15529  limcresi  15531  cnplimcim  15532  cnplimclemle  15533  cnplimclemr  15534  limccnpcntop  15540  limccoap  15543  dvcoapbr  15572  dvcj  15574  plyf  15602  plyaddlem1  15612  plymullem1  15613  plyco  15624  plycj  15626  plycn  15627  plyrecj  15628  dvply2g  15631  efltlemlt  15639  sin0pilem2  15647  tangtx  15703  logdivlti  15746  rplogbval  15810  logbgcd1irraplemexp  15833  logbgcd1irraplemap  15834  logbgcd1irrap  15835  perfect1  15866  perfectlem1  15867  perfectlem2  15868  lgsval4a  15895  lgsdir2lem3  15903  lgsne0  15911  gausslemma2dlem3  15936  gausslemma2dlem4  15937  gausslemma2dlem6  15940  gausslemma2dlem7  15941  gausslemma2d  15942  lgseisenlem1  15943  lgsquadlem2  15951  lgsquadlem3  15952  lgsquad2lem2  15955  lgsquad3  15957  2lgsoddprmlem2  15979  2sqlem8a  15995  2sqlem8  15996  2sqlem9  15997  lpvtx  16074  upgrex  16098  upgr1een  16119  edgupgren  16136  umgredg  16140  upgrpredgv  16141  upgredg2vtx  16143  upgredgpr  16144  uspgrf1oedg  16171  usgredg4  16210  uspgredgdomord  16224  usgr1vr  16243  wlkvtxiedg  16340  wlkvtxiedgg  16341  wlk1walkdom  16354  upgriswlkdc  16355  upgrwlkedg  16356  uspgr2wlkeq  16360  uspgr2wlkeqi  16362  umgrwlknloop  16363  eupth2lem2dc  16454  trlsegvdeglem1  16455  eupth2lem3lem4fi  16468  bj-exlimmpi  16542  uzdcinzz  16570  bj-charfundcALT  16579  bj-2inf  16708  bj-peano4  16725  bj-nn0suc  16734  pw1ndom3  16764  subctctexmid  16774  exmidcon  16780  nninfalllem1  16786  nninfsellemqall  16793  nninfomnilem  16796  nninffeq  16798  nnnninfex  16800  exmidsbthrlem  16802  sbthomlem  16805  refeq  16808  isomninnlem  16814  apdifflemr  16831  redcwlpo  16840  reap0  16843  nconstwlpolem  16851