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  437  pm2.21dd  629  mt2d  634  mpnanrd  704  mpjaod  730  stdcndcOLD  858  impidc  870  jadc  875  pm2.54dc  903  oplem1  988  mp3and  1381  xor3dc  1436  exlimdd  1925  exlimddv  1954  eqrdav  2237  necon1aidc  2471  necon1bidc  2472  necon4aidc  2488  reximddv  2653  reximssdv  2654  rexlimddv  2673  vtoclgft  2873  rspcedvd  2935  sseldd  3249  ssneldd  3251  tpid3g  3823  preq12b  3890  axpweq  4303  exmid1dc  4332  exmid1stab  4340  opth  4372  issod  4459  frirrg  4490  frind  4492  ralxfr2d  4605  rexxfr2d  4606  eldifpw  4618  onun2  4632  onuni  4636  elirr  4683  en2lp  4696  wetriext  4719  peano2  4737  relop  4925  elres  5094  sotri2  5180  iota4an  5353  iota5  5354  funeu  5397  funopg  5406  imadiflem  5455  funimaexglem  5459  ssimaex  5758  ffvelcdm  5832  dff3im  5844  dffo4  5847  funopsn  5882  f1eqcocnv  5987  f1oiso2  6023  riota5f  6055  riotass2  6057  acexmidlemcase  6070  elovimad  6119  ovmpodf  6210  ovmpodv2  6212  ovi3  6216  ov6g  6217  caoftrn  6325  op1steq  6403  fvdifsuppst  6474  suppssdc  6490  suppofss1dcl  6494  suppofss2dcl  6495  tfr0dm  6583  tfrlemibxssdm  6588  tfrlemi14d  6594  tfr1onlembxssdm  6604  tfr1onlemaccex  6609  tfr1onlemres  6610  tfrcllembxssdm  6617  tfrcllemaccex  6622  tfrcllemres  6623  rdgivallem  6642  nnsucelsuc  6754  nnsucsssuc  6755  dcdifsnid  6767  nnawordex  6792  ersym  6809  mapvalg  6922  pmvalg  6923  mapsnd  6960  mapsn  6962  fundmen  7084  1dom1el  7097  en2  7102  pw2f1odclem  7124  mapdom1g  7137  fidceq  7161  fin0or  7180  findcard2  7183  findcard2s  7184  fidcen  7193  prfidceq  7225  fiintim  7228  suplub2ti  7331  supsnti  7335  supisoex  7339  difinfsnlem  7429  difinfsn  7430  ctm  7439  ctssdclemn0  7440  ctssdccl  7441  ctssdc  7443  enumctlemm  7444  nninfninc  7453  nnnninfeq2  7459  enomnilem  7468  exmidomniim  7471  exmidomni  7472  fodjuomnilemdc  7474  fodjuomnilemres  7478  omnimkv  7486  mkvprop  7488  omniwomnimkv  7497  en2prde  7529  pr2cv1  7531  en2eleq  7537  acfun  7553  exmidontriimlem1  7567  exmidontriimlem4  7570  exmidontriim  7571  papsym  7602  papcotr  7603  ccfunen  7620  cc4f  7625  cc4n  7627  elni2  7671  mulclpi  7685  nlt1pig  7698  indpi  7699  recclnq  7749  ltexnqq  7765  halfnqq  7767  prarloclemarch  7775  prarloclemarch2  7776  prop  7832  prltlu  7844  prarloclem3step  7853  prarloclem5  7857  prarloclem  7858  prarloc  7860  prarloc2  7861  genpml  7874  genpmu  7875  genprndl  7878  genprndu  7879  genpdisj  7880  addnqprllem  7884  addnqprulem  7885  addlocprlemeq  7890  addlocprlemgt  7891  addlocprlem  7892  addlocpr  7893  nqprloc  7902  nqprl  7908  nqpru  7909  addnqprlemrl  7914  addnqprlemru  7915  appdivnq  7920  prmuloc  7923  prmuloc2  7924  mullocprlem  7927  mullocpr  7928  mulnqprlemrl  7930  mulnqprlemru  7931  ltprordil  7946  ltpopr  7952  ltsopr  7953  ltaddpr  7954  ltexprlemm  7957  ltexprlemopl  7958  ltexprlemlol  7959  ltexprlemopu  7960  ltexprlemupu  7961  ltexprlemloc  7964  ltexprlemfl  7966  ltexprlemrl  7967  ltexprlemfu  7968  ltexprlemru  7969  ltaprg  7976  recexprlemm  7981  recexprlem1ssl  7990  recexprlem1ssu  7991  aptiprleml  7996  aptiprlemu  7997  archpr  8000  cauappcvgprlemm  8002  cauappcvgprlemopl  8003  cauappcvgprlemlol  8004  cauappcvgprlemopu  8005  cauappcvgprlemupu  8006  cauappcvgprlemdisj  8008  cauappcvgprlemloc  8009  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  cauappcvgprlemladdru  8013  cauappcvgprlem1  8016  archrecpr  8021  caucvgprlemnkj  8023  caucvgprlemnbj  8024  caucvgprlemm  8025  caucvgprlemopl  8026  caucvgprlemlol  8027  caucvgprlemopu  8028  caucvgprlemupu  8029  caucvgprlemdisj  8031  caucvgprlemloc  8032  caucvgprlemladdfu  8034  caucvgprlem1  8036  caucvgprlemlim  8038  caucvgprprlemnbj  8050  caucvgprprlemml  8051  caucvgprprlemopl  8054  caucvgprprlemlol  8055  caucvgprprlemopu  8056  caucvgprprlemupu  8057  caucvgprprlemdisj  8059  caucvgprprlemloc  8060  caucvgprprlemexbt  8063  caucvgprprlemaddq  8065  caucvgprprlemlim  8068  suplocexprlemss  8072  suplocexprlemrl  8074  suplocexprlemmu  8075  suplocexprlemru  8076  suplocexprlemdisj  8077  suplocexprlemloc  8078  suplocexprlemub  8080  suplocexprlemlub  8081  recexgt0sr  8130  mulgt0sr  8135  archsr  8139  caucvgsrlemoffcau  8155  suplocsrlemb  8163  suplocsrlempr  8164  suplocsrlem  8165  cnm  8189  axarch  8248  axcaucvglemcau  8255  axpre-suploclemres  8258  lelttr  8404  ltletr  8405  ltled  8435  cnegexlem1  8491  cnegexlem2  8492  renegcl  8577  negf1o  8699  gt0add  8891  apreap  8905  apirr  8923  apsym  8924  apcotr  8925  apadd1  8926  apneg  8929  mulext1  8930  mulap0r  8933  apti  8940  aprcl  8964  aptap  8968  recexap  8971  mulap0  8972  receuap  8989  mul0eqap  8990  lep1  9165  lem1  9167  letrp1  9168  recreclt  9220  lbinf  9268  suprubex  9271  nnrecgt0  9321  bndndx  9541  nn0ge2m1nn  9606  elnn0z  9636  peano2z  9659  zaddcl  9663  ztri3or0  9665  zltnle  9669  zdceq  9699  zdcle  9700  zdclt  9701  zdiv  9713  zeo  9730  fnn0ind  9741  btwnz  9744  uzm1  9932  uzp1  9935  indstr  9972  supinfneg  9974  infsupneg  9975  eluzdc  9989  nn01to3  9996  qapne  10018  xrltled  10180  xrlelttr  10187  xrltletr  10188  ge0nemnf  10205  fzdcel  10423  elfzouz2  10547  fzoss1  10558  fzospliti  10563  elincfzoext  10589  fzocatel  10595  fzostep1  10634  zsupcllemstep  10640  zsupcl  10642  infssuzledc  10645  qtri3or  10653  qltnle  10656  qdceq  10657  qdclt  10658  exbtwnzlemex  10662  rebtwn2zlemstep  10665  rebtwn2z  10667  qbtwnxr  10670  ioom  10673  ico0  10674  ioc0  10675  flqeqceilz  10733  modqadd1  10776  modqmul1  10792  frec2uzuzd  10817  frec2uzlt2d  10819  frec2uzf1od  10821  frecuzrdgrrn  10823  frec2uzrdg  10824  frecuzrdgrcl  10825  frecuzrdgsuc  10829  frecuzrdgrclt  10830  frecuzrdgdomlem  10832  uzsinds  10859  seqvalcd  10876  seqovcd  10882  seq3fveq2  10890  seqfveq2g  10892  seq3shft2  10896  seqshft2g  10897  monoord  10900  seq3split  10903  seqsplitg  10904  seq3caopr3  10906  iseqf1olemab  10917  iseqf1olemnanb  10918  iseqf1olemqk  10922  seqf1oglem1  10934  seqf1og  10936  seq3id3  10939  seq3id2  10941  seq3homo  10942  seqhomog  10945  expgt1  10992  m1expeven  11001  expnbnd  11079  expnlbnd2  11081  nn0ltexp2  11125  apexp1  11134  hashennn  11197  hashfibclem  11260  hashf1lem2  11264  zfz1isolem1  11270  seq3coll  11272  pfxwrdsymbg  11440  wrdind  11472  wrd2ind  11473  cjap  11650  caucvgre  11725  cvg1nlemres  11729  resqrexlemgt0  11764  resqrexlemglsq  11766  resqrexlemga  11767  resqrtcl  11773  abslt  11832  abssubap0  11834  abssubne0  11835  caubnd2  11861  qdenre  11946  maxabslemlub  11951  maxabs  11953  maxleast  11957  fimaxre2  11971  xrmaxiflemlub  11992  xrmaxif  11995  xrmaxltsup  12002  xrmaxadd  12005  xrmineqinf  12013  climuni  12037  2clim  12045  climcn1  12052  climcn2  12053  subcn2  12055  mulcn2  12056  climsqz  12079  climsqz2  12080  climcau  12091  climcvg1nlem  12093  climcaucn  12095  serf0  12096  sumrbdclem  12122  summodclem2  12127  zsumdc  12129  divcnv  12242  absltap  12254  absgtap  12255  mertenslem2  12281  ntrivcvgap  12293  prodrbdclem  12316  prodmodclem2  12322  zproddc  12324  prodssdc  12334  fprodsplitdc  12341  fprodcl2lem  12350  efcllemp  12403  tanvalap  12453  sin01bnd  12502  cos01bnd  12503  sin01gt0  12507  absef  12515  eirrap  12523  dvds0  12551  dvdsmul1  12558  dvdsmultr1d  12577  dvdslelemd  12588  divconjdvds  12594  alzdvds  12599  3dvds  12609  sqoddm1div8z  12631  nno  12651  divalglemex  12667  bits0o  12695  dvdsbnd  12711  dvdslegcd  12719  zeqzmulgcd  12725  gcd0id  12734  gcdaddm  12739  gcd1  12742  gcdabs  12743  bezoutlemnewy  12751  bezoutlemstep  12752  bezoutlemmain  12753  bezoutlemex  12756  bezoutlemzz  12757  bezoutlemaz  12758  bezoutlembz  12759  bezoutlembi  12760  bezoutlemle  12763  bezoutlemsup  12764  mulgcd  12771  gcdzeq  12777  dvdsmulgcd  12780  sqgcd  12784  bezoutr1  12788  nninfctlemfo  12795  algcvga  12807  algfx  12808  eucalglt  12813  eucalg  12815  lcmneg  12830  lcmabs  12832  lcmgcdlem  12833  ncoprmgcdne1b  12845  mulgcddvds  12850  qredeq  12852  divgcdcoprm0  12857  cncongr1  12859  isprm2lem  12872  nprm  12879  dvdsnprmd  12881  prmdvdsfz  12895  isprm5lem  12897  coprm  12900  isprm6  12903  sqrt2irr  12918  pw2dvdslemn  12921  pw2dvdseulemle  12923  oddpwdclemdvds  12926  oddpwdclemndvds  12927  sqrt2irrap  12936  qnumdencl  12943  prmdiv  12991  modprmn0modprm0  13013  prm23lt5  13020  pythagtriplem4  13025  pythagtriplem19  13039  pythagtrip  13040  pclemub  13044  pcpre1  13049  pcpremul  13050  pceulem  13051  pcqcl  13063  pcidlem  13080  pcgcd1  13085  pc2dvds  13087  dvdsprmpweqle  13094  difsqpwdvds  13095  pcadd  13097  pcmpt  13100  expnprm  13110  pockthg  13114  infpnlem2  13117  prmunb  13119  1arith  13124  4sqlem10  13144  4sqlem11  13158  4sqlem12  13159  4sqlem13m  13160  4sqlem17  13164  4sqlem18  13165  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemfrceq  13250  ennnfonelemex  13283  ennnfonelemhom  13284  ennnfonelemrnh  13285  ennnfonelemnn0  13291  ennnfonelemim  13293  exmidunben  13295  ctinfomlemom  13296  ctinfom  13297  ctinf  13299  omctfn  13312  nninfdclemp1  13319  setscomd  13371  imasaddfnlemg  13612  mhmf1o  13754  grpinveu  13820  grpasscan1  13845  dfgrp3mlem  13880  grp1inv  13889  issubg4m  13973  ghmf1o  14055  srgisid  14264  ringadd2  14305  ringinvnzdiv  14328  unitgrp  14396  ringelnzr  14467  lringuplu  14476  subrguss  14517  subrgintm  14524  aprcotr  14570  islmodd  14602  lssclg  14673  lss0cl  14678  lssvneln0  14682  lss1d  14692  lmodindp1  14737  rnglidlmmgm  14805  znidomb  14965  znunit  14966  znrrg  14967  mplsubgfilemcl  15013  mplsubgfileminv  15014  tgcl  15088  neii1  15171  neii2  15173  neiss  15174  tpnei  15184  tgrest  15193  ssrest  15206  icnpimaex  15235  lmcvg  15241  cnpnei  15243  cnptopco  15246  lmff  15273  txcnp  15295  txcn  15299  hmeontr  15337  blssec  15462  mopni3  15508  blsscls2  15517  comet  15523  bdxmet  15525  bdmopn  15528  xmettxlem  15533  xmettx  15534  addcncntoplem  15585  mpomulcn  15590  mulc1cncf  15613  cncfco  15615  cncfmptc  15620  mulcncflem  15631  mulcncf  15632  dedekindeulemlu  15645  dedekindeulemeu  15646  suplociccreex  15648  suplociccex  15649  dedekindicclemlu  15654  dedekindicclemeu  15655  ivthinclemlopn  15660  ivthinclemlr  15661  ivthinclemuopn  15662  ivthinclemur  15663  ivthinclemloc  15665  ivthinc  15667  ivthreinc  15669  ivthdichlem  15675  limcimolemlt  15688  limcresi  15690  cnplimcim  15691  cnplimclemle  15692  cnplimclemr  15693  limccnpcntop  15699  limccoap  15702  dvcoapbr  15731  dvcj  15733  plyf  15761  plyaddlem1  15771  plymullem1  15772  plyco  15783  plycj  15785  plycn  15786  plyrecj  15787  dvply2g  15790  efltlemlt  15798  sin0pilem2  15806  tangtx  15862  logdivlti  15905  rplogbval  15970  logbgcd1irraplemexp  15993  logbgcd1irraplemap  15994  logbgcd1irrap  15995  perfect1  16026  perfectlem1  16027  perfectlem2  16028  lgsval4a  16055  lgsdir2lem3  16063  lgsne0  16071  gausslemma2dlem3  16096  gausslemma2dlem4  16097  gausslemma2dlem6  16100  gausslemma2dlem7  16101  gausslemma2d  16102  lgseisenlem1  16103  lgsquadlem2  16111  lgsquadlem3  16112  lgsquad2lem2  16115  lgsquad3  16117  2lgsoddprmlem2  16139  2sqlem8a  16155  2sqlem8  16156  2sqlem9  16157  lpvtx  16234  upgrex  16258  upgr1een  16279  edgupgren  16296  umgredg  16300  upgrpredgv  16301  upgredg2vtx  16303  upgredgpr  16304  uspgrf1oedg  16331  usgredg4  16370  uspgredgdomord  16384  usgr1vr  16403  wlkvtxiedg  16500  wlkvtxiedgg  16501  wlk1walkdom  16514  upgriswlkdc  16515  upgrwlkedg  16516  uspgr2wlkeq  16520  uspgr2wlkeqi  16522  umgrwlknloop  16523  eupth2lem2dc  16614  trlsegvdeglem1  16615  eupth2lem3lem4fi  16628  bj-exlimmpi  16712  uzdcinzz  16740  bj-charfundcALT  16749  bj-2inf  16878  bj-peano4  16895  bj-nn0suc  16904  pw1ndom3  16934  subctctexmid  16944  exmidcon  16950  nninfalllem1  16956  nninfsellemqall  16963  nninfomnilem  16966  nninffeq  16968  nnnninfex  16970  exmidsbthrlem  16972  sbthomlem  16975  refeq  16978  isomninnlem  16984  apdifflemr  17001  redcwlpo  17010  reap0  17013  nconstwlpolem  17020