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  146  mpbird  166  jcai  309  mp2and  431  pm2.21dd  615  mt2d  620  mpjaod  713  stdcndcOLD  841  impidc  853  jadc  858  pm2.54dc  886  pm4.55dc  933  oplem1  970  mp3and  1335  xor3dc  1382  exlimdd  1865  exlimddv  1891  eqrdav  2169  necon1aidc  2391  necon1bidc  2392  necon4aidc  2408  reximddv  2573  reximssdv  2574  rexlimddv  2592  vtoclgft  2780  rspcedvd  2840  sseldd  3148  ssneldd  3150  tpid3g  3698  preq12b  3757  axpweq  4157  exmid1dc  4186  opth  4222  issod  4304  frirrg  4335  frind  4337  ralxfr2d  4449  rexxfr2d  4450  eldifpw  4462  onun2  4474  onuni  4478  elirr  4525  en2lp  4538  wetriext  4561  peano2  4579  relop  4761  elres  4927  sotri2  5008  iota4an  5179  iota5  5180  funeu  5223  funopg  5232  imadiflem  5277  funimaexglem  5281  ssimaex  5557  ffvelrn  5629  dff3im  5641  dffo4  5644  f1eqcocnv  5770  f1oiso2  5806  riota5f  5833  riotass2  5835  acexmidlemcase  5848  ovmpodf  5984  ovmpodv2  5986  ovi3  5989  ov6g  5990  caoftrn  6086  op1steq  6158  tfr0dm  6301  tfrlemibxssdm  6306  tfrlemi14d  6312  tfr1onlembxssdm  6322  tfr1onlemaccex  6327  tfr1onlemres  6328  tfrcllembxssdm  6335  tfrcllemaccex  6340  tfrcllemres  6341  rdgivallem  6360  nnsucelsuc  6470  nnsucsssuc  6471  dcdifsnid  6483  nnawordex  6508  ersym  6525  mapvalg  6636  pmvalg  6637  mapsn  6668  fundmen  6784  mapdom1g  6825  fidceq  6847  fin0or  6864  findcard2  6867  findcard2s  6868  fiintim  6906  suplub2ti  6978  supsnti  6982  supisoex  6986  difinfsnlem  7076  difinfsn  7077  ctm  7086  ctssdclemn0  7087  ctssdccl  7088  ctssdc  7090  enumctlemm  7091  nnnninfeq2  7105  enomnilem  7114  exmidomniim  7117  exmidomni  7118  fodjuomnilemdc  7120  fodjuomnilemres  7124  omnimkv  7132  mkvprop  7134  omniwomnimkv  7143  en2eleq  7172  acfun  7184  exmidontriimlem1  7198  exmidontriimlem4  7201  exmidontriim  7202  ccfunen  7226  cc4f  7231  cc4n  7233  elni2  7276  mulclpi  7290  nlt1pig  7303  indpi  7304  recclnq  7354  ltexnqq  7370  halfnqq  7372  prarloclemarch  7380  prarloclemarch2  7381  prop  7437  prltlu  7449  prarloclem3step  7458  prarloclem5  7462  prarloclem  7463  prarloc  7465  prarloc2  7466  genpml  7479  genpmu  7480  genprndl  7483  genprndu  7484  genpdisj  7485  addnqprllem  7489  addnqprulem  7490  addlocprlemeq  7495  addlocprlemgt  7496  addlocprlem  7497  addlocpr  7498  nqprloc  7507  nqprl  7513  nqpru  7514  addnqprlemrl  7519  addnqprlemru  7520  appdivnq  7525  prmuloc  7528  prmuloc2  7529  mullocprlem  7532  mullocpr  7533  mulnqprlemrl  7535  mulnqprlemru  7536  ltprordil  7551  ltpopr  7557  ltsopr  7558  ltaddpr  7559  ltexprlemm  7562  ltexprlemopl  7563  ltexprlemlol  7564  ltexprlemopu  7565  ltexprlemupu  7566  ltexprlemloc  7569  ltexprlemfl  7571  ltexprlemrl  7572  ltexprlemfu  7573  ltexprlemru  7574  ltaprg  7581  recexprlemm  7586  recexprlem1ssl  7595  recexprlem1ssu  7596  aptiprleml  7601  aptiprlemu  7602  archpr  7605  cauappcvgprlemm  7607  cauappcvgprlemopl  7608  cauappcvgprlemlol  7609  cauappcvgprlemopu  7610  cauappcvgprlemupu  7611  cauappcvgprlemdisj  7613  cauappcvgprlemloc  7614  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  cauappcvgprlemladdru  7618  cauappcvgprlem1  7621  archrecpr  7626  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprlemm  7630  caucvgprlemopl  7631  caucvgprlemlol  7632  caucvgprlemopu  7633  caucvgprlemupu  7634  caucvgprlemdisj  7636  caucvgprlemloc  7637  caucvgprlemladdfu  7639  caucvgprlem1  7641  caucvgprlemlim  7643  caucvgprprlemnbj  7655  caucvgprprlemml  7656  caucvgprprlemopl  7659  caucvgprprlemlol  7660  caucvgprprlemopu  7661  caucvgprprlemupu  7662  caucvgprprlemdisj  7664  caucvgprprlemloc  7665  caucvgprprlemexbt  7668  caucvgprprlemaddq  7670  caucvgprprlemlim  7673  suplocexprlemss  7677  suplocexprlemrl  7679  suplocexprlemmu  7680  suplocexprlemru  7681  suplocexprlemdisj  7682  suplocexprlemloc  7683  suplocexprlemub  7685  suplocexprlemlub  7686  recexgt0sr  7735  mulgt0sr  7740  archsr  7744  caucvgsrlemoffcau  7760  suplocsrlemb  7768  suplocsrlempr  7769  suplocsrlem  7770  cnm  7794  axarch  7853  axcaucvglemcau  7860  axpre-suploclemres  7863  lelttr  8008  ltletr  8009  ltled  8038  cnegexlem1  8094  cnegexlem2  8095  renegcl  8180  negf1o  8301  gt0add  8492  apreap  8506  apirr  8524  apsym  8525  apcotr  8526  apadd1  8527  apneg  8530  mulext1  8531  mulap0r  8534  apti  8541  aprcl  8565  recexap  8571  mulap0  8572  receuap  8587  mul0eqap  8588  lep1  8761  lem1  8763  letrp1  8764  recreclt  8816  lbinf  8864  suprubex  8867  nnrecgt0  8916  bndndx  9134  nn0ge2m1nn  9195  elnn0z  9225  peano2z  9248  zaddcl  9252  ztri3or0  9254  zltnle  9258  zdceq  9287  zdcle  9288  zdclt  9289  zdiv  9300  zeo  9317  fnn0ind  9328  btwnz  9331  uzm1  9517  uzp1  9520  indstr  9552  supinfneg  9554  infsupneg  9555  eluzdc  9569  nn01to3  9576  qapne  9598  xrltled  9756  xrlelttr  9763  xrltletr  9764  ge0nemnf  9781  fzdcel  9996  elfzouz2  10117  fzoss1  10127  fzospliti  10132  fzocatel  10155  fzostep1  10193  qtri3or  10199  qltnle  10202  qdceq  10203  exbtwnzlemex  10206  rebtwn2zlemstep  10209  rebtwn2z  10211  qbtwnxr  10214  ioom  10217  ico0  10218  ioc0  10219  flqeqceilz  10274  modqadd1  10317  modqmul1  10333  frec2uzuzd  10358  frec2uzlt2d  10360  frec2uzf1od  10362  frecuzrdgrrn  10364  frec2uzrdg  10365  frecuzrdgrcl  10366  frecuzrdgsuc  10370  frecuzrdgrclt  10371  frecuzrdgdomlem  10373  uzsinds  10398  seqvalcd  10415  seqovcd  10419  seq3fveq2  10425  seq3shft2  10429  monoord  10432  seq3split  10435  seq3caopr3  10437  iseqf1olemab  10445  iseqf1olemnanb  10446  iseqf1olemqk  10450  seq3id3  10463  seq3id2  10465  seq3homo  10466  expgt1  10514  m1expeven  10523  expnbnd  10599  expnlbnd2  10601  nn0ltexp2  10644  apexp1  10652  hashennn  10714  zfz1isolem1  10775  seq3coll  10777  cjap  10870  caucvgre  10945  cvg1nlemres  10949  resqrexlemgt0  10984  resqrexlemglsq  10986  resqrexlemga  10987  resqrtcl  10993  abslt  11052  abssubap0  11054  abssubne0  11055  caubnd2  11081  qdenre  11166  maxabslemlub  11171  maxabs  11173  maxleast  11177  fimaxre2  11190  xrmaxiflemlub  11211  xrmaxif  11214  xrmaxltsup  11221  xrmaxadd  11224  xrmineqinf  11232  climuni  11256  2clim  11264  climcn1  11271  climcn2  11272  subcn2  11274  mulcn2  11275  climsqz  11298  climsqz2  11299  climcau  11310  climcvg1nlem  11312  climcaucn  11314  serf0  11315  sumrbdclem  11340  summodclem2  11345  zsumdc  11347  divcnv  11460  absltap  11472  absgtap  11473  mertenslem2  11499  ntrivcvgap  11511  prodrbdclem  11534  prodmodclem2  11540  zproddc  11542  prodssdc  11552  fprodsplitdc  11559  fprodcl2lem  11568  efcllemp  11621  tanvalap  11671  sin01bnd  11720  cos01bnd  11721  sin01gt0  11724  absef  11732  eirrap  11740  dvds0  11768  dvdsmul1  11775  dvdsmultr1d  11794  dvdslelemd  11803  divconjdvds  11809  alzdvds  11814  sqoddm1div8z  11845  nno  11865  divalglemex  11881  zsupcllemstep  11900  zsupcl  11902  infssuzledc  11905  dvdsbnd  11911  dvdslegcd  11919  zeqzmulgcd  11925  gcd0id  11934  gcdaddm  11939  gcd1  11942  gcdabs  11943  bezoutlemnewy  11951  bezoutlemstep  11952  bezoutlemmain  11953  bezoutlemex  11956  bezoutlemzz  11957  bezoutlemaz  11958  bezoutlembz  11959  bezoutlembi  11960  bezoutlemle  11963  bezoutlemsup  11964  mulgcd  11971  gcdzeq  11977  dvdsmulgcd  11980  sqgcd  11984  bezoutr1  11988  algcvga  12005  algfx  12006  eucalglt  12011  eucalg  12013  lcmneg  12028  lcmabs  12030  lcmgcdlem  12031  ncoprmgcdne1b  12043  mulgcddvds  12048  qredeq  12050  divgcdcoprm0  12055  cncongr1  12057  isprm2lem  12070  nprm  12077  dvdsnprmd  12079  prmdvdsfz  12093  isprm5lem  12095  coprm  12098  isprm6  12101  sqrt2irr  12116  pw2dvdslemn  12119  pw2dvdseulemle  12121  oddpwdclemdvds  12124  oddpwdclemndvds  12125  sqrt2irrap  12134  qnumdencl  12141  prmdiv  12189  modprmn0modprm0  12210  prm23lt5  12217  pythagtriplem4  12222  pythagtriplem19  12236  pythagtrip  12237  pclemub  12241  pcpre1  12246  pcpremul  12247  pceulem  12248  pcqcl  12260  pcidlem  12276  pcgcd1  12281  pc2dvds  12283  dvdsprmpweqle  12290  difsqpwdvds  12291  pcadd  12293  pcmpt  12295  expnprm  12305  pockthg  12309  infpnlem2  12312  prmunb  12314  1arith  12319  4sqlem10  12339  ennnfonelemex  12369  ennnfonelemhom  12370  ennnfonelemrnh  12371  ennnfonelemnn0  12377  ennnfonelemim  12379  exmidunben  12381  ctinfomlemom  12382  ctinfom  12383  ctinf  12385  omctfn  12398  nninfdclemp1  12405  mhmf1o  12693  grpinveu  12741  grpasscan1  12762  tgcl  12858  neii1  12941  neii2  12943  neiss  12944  tpnei  12954  tgrest  12963  ssrest  12976  icnpimaex  13005  lmcvg  13011  cnpnei  13013  cnptopco  13016  lmff  13043  txcnp  13065  txcn  13069  hmeontr  13107  blssec  13232  mopni3  13278  blsscls2  13287  comet  13293  bdxmet  13295  bdmopn  13298  xmettxlem  13303  xmettx  13304  addcncntoplem  13345  mulc1cncf  13370  cncfco  13372  cncfmptc  13376  mulcncflem  13384  mulcncf  13385  dedekindeulemlu  13393  dedekindeulemeu  13394  suplociccreex  13396  suplociccex  13397  dedekindicclemlu  13402  dedekindicclemeu  13403  ivthinclemlopn  13408  ivthinclemlr  13409  ivthinclemuopn  13410  ivthinclemur  13411  ivthinclemloc  13413  ivthinc  13415  limcimolemlt  13427  limcresi  13429  cnplimcim  13430  cnplimclemle  13431  cnplimclemr  13432  limccnpcntop  13438  limccoap  13441  dvcoapbr  13465  dvcj  13467  efltlemlt  13489  sin0pilem2  13497  tangtx  13553  logdivlti  13596  rplogbval  13657  logbgcd1irraplemexp  13680  logbgcd1irraplemap  13681  logbgcd1irrap  13682  lgsval4a  13717  lgsdir2lem3  13725  lgsne0  13733  2sqlem8a  13752  2sqlem8  13753  2sqlem9  13754  bj-exlimmpi  13805  uzdcinzz  13833  bj-charfundcALT  13844  bj-2inf  13973  bj-peano4  13990  bj-nn0suc  13999  exmid1stab  14033  subctctexmid  14034  nninfalllem1  14041  nninfsellemqall  14048  nninfomnilem  14051  nninffeq  14053  exmidsbthrlem  14054  sbthomlem  14057  refeq  14060  isomninnlem  14062  apdifflemr  14079  redcwlpo  14087  reap0  14090  nconstwlpolem  14096