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  620  mt2d  625  mpjaod  718  stdcndcOLD  846  impidc  858  jadc  863  pm2.54dc  891  pm4.55dc  938  oplem1  975  mp3and  1340  xor3dc  1387  exlimdd  1872  exlimddv  1898  eqrdav  2176  necon1aidc  2398  necon1bidc  2399  necon4aidc  2415  reximddv  2580  reximssdv  2581  rexlimddv  2599  vtoclgft  2788  rspcedvd  2848  sseldd  3157  ssneldd  3159  tpid3g  3708  preq12b  3771  axpweq  4172  exmid1dc  4201  exmid1stab  4209  opth  4238  issod  4320  frirrg  4351  frind  4353  ralxfr2d  4465  rexxfr2d  4466  eldifpw  4478  onun2  4490  onuni  4494  elirr  4541  en2lp  4554  wetriext  4577  peano2  4595  relop  4778  elres  4944  sotri2  5027  iota4an  5198  iota5  5199  funeu  5242  funopg  5251  imadiflem  5296  funimaexglem  5300  ssimaex  5578  ffvelcdm  5650  dff3im  5662  dffo4  5665  f1eqcocnv  5792  f1oiso2  5828  riota5f  5855  riotass2  5857  acexmidlemcase  5870  ovmpodf  6006  ovmpodv2  6008  ovi3  6011  ov6g  6012  caoftrn  6108  op1steq  6180  tfr0dm  6323  tfrlemibxssdm  6328  tfrlemi14d  6334  tfr1onlembxssdm  6344  tfr1onlemaccex  6349  tfr1onlemres  6350  tfrcllembxssdm  6357  tfrcllemaccex  6362  tfrcllemres  6363  rdgivallem  6382  nnsucelsuc  6492  nnsucsssuc  6493  dcdifsnid  6505  nnawordex  6530  ersym  6547  mapvalg  6658  pmvalg  6659  mapsn  6690  fundmen  6806  mapdom1g  6847  fidceq  6869  fin0or  6886  findcard2  6889  findcard2s  6890  fiintim  6928  suplub2ti  7000  supsnti  7004  supisoex  7008  difinfsnlem  7098  difinfsn  7099  ctm  7108  ctssdclemn0  7109  ctssdccl  7110  ctssdc  7112  enumctlemm  7113  nnnninfeq2  7127  enomnilem  7136  exmidomniim  7139  exmidomni  7140  fodjuomnilemdc  7142  fodjuomnilemres  7146  omnimkv  7154  mkvprop  7156  omniwomnimkv  7165  en2eleq  7194  acfun  7206  exmidontriimlem1  7220  exmidontriimlem4  7223  exmidontriim  7224  ccfunen  7263  cc4f  7268  cc4n  7270  elni2  7313  mulclpi  7327  nlt1pig  7340  indpi  7341  recclnq  7391  ltexnqq  7407  halfnqq  7409  prarloclemarch  7417  prarloclemarch2  7418  prop  7474  prltlu  7486  prarloclem3step  7495  prarloclem5  7499  prarloclem  7500  prarloc  7502  prarloc2  7503  genpml  7516  genpmu  7517  genprndl  7520  genprndu  7521  genpdisj  7522  addnqprllem  7526  addnqprulem  7527  addlocprlemeq  7532  addlocprlemgt  7533  addlocprlem  7534  addlocpr  7535  nqprloc  7544  nqprl  7550  nqpru  7551  addnqprlemrl  7556  addnqprlemru  7557  appdivnq  7562  prmuloc  7565  prmuloc2  7566  mullocprlem  7569  mullocpr  7570  mulnqprlemrl  7572  mulnqprlemru  7573  ltprordil  7588  ltpopr  7594  ltsopr  7595  ltaddpr  7596  ltexprlemm  7599  ltexprlemopl  7600  ltexprlemlol  7601  ltexprlemopu  7602  ltexprlemupu  7603  ltexprlemloc  7606  ltexprlemfl  7608  ltexprlemrl  7609  ltexprlemfu  7610  ltexprlemru  7611  ltaprg  7618  recexprlemm  7623  recexprlem1ssl  7632  recexprlem1ssu  7633  aptiprleml  7638  aptiprlemu  7639  archpr  7642  cauappcvgprlemm  7644  cauappcvgprlemopl  7645  cauappcvgprlemlol  7646  cauappcvgprlemopu  7647  cauappcvgprlemupu  7648  cauappcvgprlemdisj  7650  cauappcvgprlemloc  7651  cauappcvgprlemladdfu  7653  cauappcvgprlemladdfl  7654  cauappcvgprlemladdru  7655  cauappcvgprlem1  7658  archrecpr  7663  caucvgprlemnkj  7665  caucvgprlemnbj  7666  caucvgprlemm  7667  caucvgprlemopl  7668  caucvgprlemlol  7669  caucvgprlemopu  7670  caucvgprlemupu  7671  caucvgprlemdisj  7673  caucvgprlemloc  7674  caucvgprlemladdfu  7676  caucvgprlem1  7678  caucvgprlemlim  7680  caucvgprprlemnbj  7692  caucvgprprlemml  7693  caucvgprprlemopl  7696  caucvgprprlemlol  7697  caucvgprprlemopu  7698  caucvgprprlemupu  7699  caucvgprprlemdisj  7701  caucvgprprlemloc  7702  caucvgprprlemexbt  7705  caucvgprprlemaddq  7707  caucvgprprlemlim  7710  suplocexprlemss  7714  suplocexprlemrl  7716  suplocexprlemmu  7717  suplocexprlemru  7718  suplocexprlemdisj  7719  suplocexprlemloc  7720  suplocexprlemub  7722  suplocexprlemlub  7723  recexgt0sr  7772  mulgt0sr  7777  archsr  7781  caucvgsrlemoffcau  7797  suplocsrlemb  7805  suplocsrlempr  7806  suplocsrlem  7807  cnm  7831  axarch  7890  axcaucvglemcau  7897  axpre-suploclemres  7900  lelttr  8046  ltletr  8047  ltled  8076  cnegexlem1  8132  cnegexlem2  8133  renegcl  8218  negf1o  8339  gt0add  8530  apreap  8544  apirr  8562  apsym  8563  apcotr  8564  apadd1  8565  apneg  8568  mulext1  8569  mulap0r  8572  apti  8579  aprcl  8603  aptap  8607  recexap  8610  mulap0  8611  receuap  8626  mul0eqap  8627  lep1  8802  lem1  8804  letrp1  8805  recreclt  8857  lbinf  8905  suprubex  8908  nnrecgt0  8957  bndndx  9175  nn0ge2m1nn  9236  elnn0z  9266  peano2z  9289  zaddcl  9293  ztri3or0  9295  zltnle  9299  zdceq  9328  zdcle  9329  zdclt  9330  zdiv  9341  zeo  9358  fnn0ind  9369  btwnz  9372  uzm1  9558  uzp1  9561  indstr  9593  supinfneg  9595  infsupneg  9596  eluzdc  9610  nn01to3  9617  qapne  9639  xrltled  9799  xrlelttr  9806  xrltletr  9807  ge0nemnf  9824  fzdcel  10040  elfzouz2  10161  fzoss1  10171  fzospliti  10176  fzocatel  10199  fzostep1  10237  qtri3or  10243  qltnle  10246  qdceq  10247  exbtwnzlemex  10250  rebtwn2zlemstep  10253  rebtwn2z  10255  qbtwnxr  10258  ioom  10261  ico0  10262  ioc0  10263  flqeqceilz  10318  modqadd1  10361  modqmul1  10377  frec2uzuzd  10402  frec2uzlt2d  10404  frec2uzf1od  10406  frecuzrdgrrn  10408  frec2uzrdg  10409  frecuzrdgrcl  10410  frecuzrdgsuc  10414  frecuzrdgrclt  10415  frecuzrdgdomlem  10417  uzsinds  10442  seqvalcd  10459  seqovcd  10463  seq3fveq2  10469  seq3shft2  10473  monoord  10476  seq3split  10479  seq3caopr3  10481  iseqf1olemab  10489  iseqf1olemnanb  10490  iseqf1olemqk  10494  seq3id3  10507  seq3id2  10509  seq3homo  10510  expgt1  10558  m1expeven  10567  expnbnd  10644  expnlbnd2  10646  nn0ltexp2  10689  apexp1  10698  hashennn  10760  zfz1isolem1  10820  seq3coll  10822  cjap  10915  caucvgre  10990  cvg1nlemres  10994  resqrexlemgt0  11029  resqrexlemglsq  11031  resqrexlemga  11032  resqrtcl  11038  abslt  11097  abssubap0  11099  abssubne0  11100  caubnd2  11126  qdenre  11211  maxabslemlub  11216  maxabs  11218  maxleast  11222  fimaxre2  11235  xrmaxiflemlub  11256  xrmaxif  11259  xrmaxltsup  11266  xrmaxadd  11269  xrmineqinf  11277  climuni  11301  2clim  11309  climcn1  11316  climcn2  11317  subcn2  11319  mulcn2  11320  climsqz  11343  climsqz2  11344  climcau  11355  climcvg1nlem  11357  climcaucn  11359  serf0  11360  sumrbdclem  11385  summodclem2  11390  zsumdc  11392  divcnv  11505  absltap  11517  absgtap  11518  mertenslem2  11544  ntrivcvgap  11556  prodrbdclem  11579  prodmodclem2  11585  zproddc  11587  prodssdc  11597  fprodsplitdc  11604  fprodcl2lem  11613  efcllemp  11666  tanvalap  11716  sin01bnd  11765  cos01bnd  11766  sin01gt0  11769  absef  11777  eirrap  11785  dvds0  11813  dvdsmul1  11820  dvdsmultr1d  11839  dvdslelemd  11849  divconjdvds  11855  alzdvds  11860  sqoddm1div8z  11891  nno  11911  divalglemex  11927  zsupcllemstep  11946  zsupcl  11948  infssuzledc  11951  dvdsbnd  11957  dvdslegcd  11965  zeqzmulgcd  11971  gcd0id  11980  gcdaddm  11985  gcd1  11988  gcdabs  11989  bezoutlemnewy  11997  bezoutlemstep  11998  bezoutlemmain  11999  bezoutlemex  12002  bezoutlemzz  12003  bezoutlemaz  12004  bezoutlembz  12005  bezoutlembi  12006  bezoutlemle  12009  bezoutlemsup  12010  mulgcd  12017  gcdzeq  12023  dvdsmulgcd  12026  sqgcd  12030  bezoutr1  12034  algcvga  12051  algfx  12052  eucalglt  12057  eucalg  12059  lcmneg  12074  lcmabs  12076  lcmgcdlem  12077  ncoprmgcdne1b  12089  mulgcddvds  12094  qredeq  12096  divgcdcoprm0  12101  cncongr1  12103  isprm2lem  12116  nprm  12123  dvdsnprmd  12125  prmdvdsfz  12139  isprm5lem  12141  coprm  12144  isprm6  12147  sqrt2irr  12162  pw2dvdslemn  12165  pw2dvdseulemle  12167  oddpwdclemdvds  12170  oddpwdclemndvds  12171  sqrt2irrap  12180  qnumdencl  12187  prmdiv  12235  modprmn0modprm0  12256  prm23lt5  12263  pythagtriplem4  12268  pythagtriplem19  12282  pythagtrip  12283  pclemub  12287  pcpre1  12292  pcpremul  12293  pceulem  12294  pcqcl  12306  pcidlem  12322  pcgcd1  12327  pc2dvds  12329  dvdsprmpweqle  12336  difsqpwdvds  12337  pcadd  12339  pcmpt  12341  expnprm  12351  pockthg  12355  infpnlem2  12358  prmunb  12360  1arith  12365  4sqlem10  12385  ennnfonelemex  12415  ennnfonelemhom  12416  ennnfonelemrnh  12417  ennnfonelemnn0  12423  ennnfonelemim  12425  exmidunben  12427  ctinfomlemom  12428  ctinfom  12429  ctinf  12431  omctfn  12444  nninfdclemp1  12451  setscomd  12503  imasaddfnlemg  12735  mhmf1o  12861  grpinveu  12911  grpasscan1  12933  dfgrp3mlem  12968  grp1inv  12977  issubg4m  13053  srgisid  13169  ringadd2  13210  ringinvnzdiv  13227  unitgrp  13285  ringelnzr  13328  lringuplu  13337  subrguss  13357  subrgintm  13364  aprcotr  13375  islmodd  13383  tgcl  13567  neii1  13650  neii2  13652  neiss  13653  tpnei  13663  tgrest  13672  ssrest  13685  icnpimaex  13714  lmcvg  13720  cnpnei  13722  cnptopco  13725  lmff  13752  txcnp  13774  txcn  13778  hmeontr  13816  blssec  13941  mopni3  13987  blsscls2  13996  comet  14002  bdxmet  14004  bdmopn  14007  xmettxlem  14012  xmettx  14013  addcncntoplem  14054  mulc1cncf  14079  cncfco  14081  cncfmptc  14085  mulcncflem  14093  mulcncf  14094  dedekindeulemlu  14102  dedekindeulemeu  14103  suplociccreex  14105  suplociccex  14106  dedekindicclemlu  14111  dedekindicclemeu  14112  ivthinclemlopn  14117  ivthinclemlr  14118  ivthinclemuopn  14119  ivthinclemur  14120  ivthinclemloc  14122  ivthinc  14124  limcimolemlt  14136  limcresi  14138  cnplimcim  14139  cnplimclemle  14140  cnplimclemr  14141  limccnpcntop  14147  limccoap  14150  dvcoapbr  14174  dvcj  14176  efltlemlt  14198  sin0pilem2  14206  tangtx  14262  logdivlti  14305  rplogbval  14366  logbgcd1irraplemexp  14389  logbgcd1irraplemap  14390  logbgcd1irrap  14391  lgsval4a  14426  lgsdir2lem3  14434  lgsne0  14442  lgseisenlem1  14453  2lgsoddprmlem2  14457  2sqlem8a  14472  2sqlem8  14473  2sqlem9  14474  bj-exlimmpi  14525  uzdcinzz  14553  bj-charfundcALT  14564  bj-2inf  14693  bj-peano4  14710  bj-nn0suc  14719  subctctexmid  14753  nninfalllem1  14760  nninfsellemqall  14767  nninfomnilem  14770  nninffeq  14772  exmidsbthrlem  14773  sbthomlem  14776  refeq  14779  isomninnlem  14781  apdifflemr  14798  redcwlpo  14806  reap0  14809  nconstwlpolem  14815