Theorem mpd 13

Description: A modus ponens deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
mpd.1	⊢ (𝜑 → 𝜓)
mpd.2	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
mpd	⊢ (𝜑 → 𝜒)

Proof of Theorem mpd

Step	Hyp	Ref	Expression
1		mpd.1	. 2 ⊢ (𝜑 → 𝜓)
2		mpd.2	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	a2i 11	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))
4	1, 3	ax-mp 5	1 ⊢ (𝜑 → 𝜒)

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  11204  zfz1isolem1  11210  seq3coll  11212  pfxwrdsymbg  11380  wrdind  11412  wrd2ind  11413  cjap  11589  caucvgre  11664  cvg1nlemres  11668  resqrexlemgt0  11703  resqrexlemglsq  11705  resqrexlemga  11706  resqrtcl  11712  abslt  11771  abssubap0  11773  abssubne0  11774  caubnd2  11800  qdenre  11885  maxabslemlub  11890  maxabs  11892  maxleast  11896  fimaxre2  11910  xrmaxiflemlub  11931  xrmaxif  11934  xrmaxltsup  11941  xrmaxadd  11944  xrmineqinf  11952  climuni  11976  2clim  11984  climcn1  11991  climcn2  11992  subcn2  11994  mulcn2  11995  climsqz  12018  climsqz2  12019  climcau  12030  climcvg1nlem  12032  climcaucn  12034  serf0  12035  sumrbdclem  12061  summodclem2  12066  zsumdc  12068  divcnv  12181  absltap  12193  absgtap  12194  mertenslem2  12220  ntrivcvgap  12232  prodrbdclem  12255  prodmodclem2  12261  zproddc  12263  prodssdc  12273  fprodsplitdc  12280  fprodcl2lem  12289  efcllemp  12342  tanvalap  12392  sin01bnd  12441  cos01bnd  12442  sin01gt0  12446  absef  12454  eirrap  12462  dvds0  12490  dvdsmul1  12497  dvdsmultr1d  12516  dvdslelemd  12527  divconjdvds  12533  alzdvds  12538  3dvds  12548  sqoddm1div8z  12570  nno  12590  divalglemex  12606  bits0o  12634  dvdsbnd  12650  dvdslegcd  12658  zeqzmulgcd  12664  gcd0id  12673  gcdaddm  12678  gcd1  12681  gcdabs  12682  bezoutlemnewy  12690  bezoutlemstep  12691  bezoutlemmain  12692  bezoutlemex  12695  bezoutlemzz  12696  bezoutlemaz  12697  bezoutlembz  12698  bezoutlembi  12699  bezoutlemle  12702  bezoutlemsup  12703  mulgcd  12710  gcdzeq  12716  dvdsmulgcd  12719  sqgcd  12723  bezoutr1  12727  nninfctlemfo  12734  algcvga  12746  algfx  12747  eucalglt  12752  eucalg  12754  lcmneg  12769  lcmabs  12771  lcmgcdlem  12772  ncoprmgcdne1b  12784  mulgcddvds  12789  qredeq  12791  divgcdcoprm0  12796  cncongr1  12798  isprm2lem  12811  nprm  12818  dvdsnprmd  12820  prmdvdsfz  12834  isprm5lem  12836  coprm  12839  isprm6  12842  sqrt2irr  12857  pw2dvdslemn  12860  pw2dvdseulemle  12862  oddpwdclemdvds  12865  oddpwdclemndvds  12866  sqrt2irrap  12875  qnumdencl  12882  prmdiv  12930  modprmn0modprm0  12952  prm23lt5  12959  pythagtriplem4  12964  pythagtriplem19  12978  pythagtrip  12979  pclemub  12983  pcpre1  12988  pcpremul  12989  pceulem  12990  pcqcl  13002  pcidlem  13019  pcgcd1  13024  pc2dvds  13026  dvdsprmpweqle  13033  difsqpwdvds  13034  pcadd  13036  pcmpt  13039  expnprm  13049  pockthg  13053  infpnlem2  13056  prmunb  13058  1arith  13063  4sqlem10  13083  4sqlem11  13097  4sqlem12  13098  4sqlem13m  13099  4sqlem17  13103  4sqlem18  13104  ennnfonelemex  13163  ennnfonelemhom  13164  ennnfonelemrnh  13165  ennnfonelemnn0  13171  ennnfonelemim  13173  exmidunben  13175  ctinfomlemom  13176  ctinfom  13177  ctinf  13179  omctfn  13192  nninfdclemp1  13199  setscomd  13251  imasaddfnlemg  13525  mhmf1o  13681  grpinveu  13749  grpasscan1  13774  dfgrp3mlem  13809  grp1inv  13818  issubg4m  13908  ghmf1o  13990  srgisid  14128  ringadd2  14169  ringinvnzdiv  14192  unitgrp  14259  ringelnzr  14330  lringuplu  14339  subrguss  14379  subrgintm  14386  aprcotr  14429  islmodd  14439  lssclg  14510  lss0cl  14515  lssvneln0  14519  lss1d  14529  lmodindp1  14574  rnglidlmmgm  14642  znidomb  14804  znunit  14805  znrrg  14806  mplsubgfilemcl  14852  mplsubgfileminv  14853  tgcl  14927  neii1  15010  neii2  15012  neiss  15013  tpnei  15023  tgrest  15032  ssrest  15045  icnpimaex  15074  lmcvg  15080  cnpnei  15082  cnptopco  15085  lmff  15112  txcnp  15134  txcn  15138  hmeontr  15176  blssec  15301  mopni3  15347  blsscls2  15356  comet  15362  bdxmet  15364  bdmopn  15367  xmettxlem  15372  xmettx  15373  addcncntoplem  15424  mpomulcn  15429  mulc1cncf  15452  cncfco  15454  cncfmptc  15459  mulcncflem  15470  mulcncf  15471  dedekindeulemlu  15484  dedekindeulemeu  15485  suplociccreex  15487  suplociccex  15488  dedekindicclemlu  15493  dedekindicclemeu  15494  ivthinclemlopn  15499  ivthinclemlr  15500  ivthinclemuopn  15501  ivthinclemur  15502  ivthinclemloc  15504  ivthinc  15506  ivthreinc  15508  ivthdichlem  15514  limcimolemlt  15527  limcresi  15529  cnplimcim  15530  cnplimclemle  15531  cnplimclemr  15532  limccnpcntop  15538  limccoap  15541  dvcoapbr  15570  dvcj  15572  plyf  15600  plyaddlem1  15610  plymullem1  15611  plyco  15622  plycj  15624  plycn  15625  plyrecj  15626  dvply2g  15629  efltlemlt  15637  sin0pilem2  15645  tangtx  15701  logdivlti  15744  rplogbval  15808  logbgcd1irraplemexp  15831  logbgcd1irraplemap  15832  logbgcd1irrap  15833  perfect1  15864  perfectlem1  15865  perfectlem2  15866  lgsval4a  15893  lgsdir2lem3  15901  lgsne0  15909  gausslemma2dlem3  15934  gausslemma2dlem4  15935  gausslemma2dlem6  15938  gausslemma2dlem7  15939  gausslemma2d  15940  lgseisenlem1  15941  lgsquadlem2  15949  lgsquadlem3  15950  lgsquad2lem2  15953  lgsquad3  15955  2lgsoddprmlem2  15977  2sqlem8a  15993  2sqlem8  15994  2sqlem9  15995  lpvtx  16072  upgrex  16096  upgr1een  16117  edgupgren  16134  umgredg  16138  upgrpredgv  16139  upgredg2vtx  16141  upgredgpr  16142  uspgrf1oedg  16169  usgredg4  16208  uspgredgdomord  16222  usgr1vr  16241  wlkvtxiedg  16338  wlkvtxiedgg  16339  wlk1walkdom  16352  upgriswlkdc  16353  upgrwlkedg  16354  uspgr2wlkeq  16358  uspgr2wlkeqi  16360  umgrwlknloop  16361  eupth2lem2dc  16452  trlsegvdeglem1  16453  eupth2lem3lem4fi  16466  bj-exlimmpi  16540  uzdcinzz  16568  bj-charfundcALT  16577  bj-2inf  16706  bj-peano4  16723  bj-nn0suc  16732  pw1ndom3  16762  subctctexmid  16772  exmidcon  16778  nninfalllem1  16784  nninfsellemqall  16791  nninfomnilem  16794  nninffeq  16796  nnnninfex  16798  exmidsbthrlem  16800  sbthomlem  16803  refeq  16806  isomninnlem  16812  apdifflemr  16829  redcwlpo  16838  reap0  16841  nconstwlpolem  16849