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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-2 7

This theorem is used 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  3828  preq12b  3895  axpweq  4310  exmid1dc  4339  exmid1stab  4347  opth  4379  issod  4466  frirrg  4497  frind  4499  ralxfr2d  4612  rexxfr2d  4613  eldifpw  4625  onun2  4639  onuni  4643  elirr  4690  en2lp  4703  wetriext  4726  peano2  4744  relop  4932  elres  5101  sotri2  5188  iota4an  5361  iota5  5362  funeu  5405  funopg  5414  imadiflem  5463  funimaexglem  5467  ssimaex  5767  ffvelcdm  5844  dff3im  5856  dffo4  5859  funopsn  5894  f1eqcocnv  6000  f1oiso2  6036  riota5f  6068  riotass2  6070  acexmidlemcase  6083  elovimad  6132  ovmpodf  6223  ovmpodv2  6225  ovi3  6229  ov6g  6230  caoftrn  6339  op1steq  6417  fvdifsuppst  6488  suppssdc  6504  suppofss1dcl  6508  suppofss2dcl  6509  tfr0dm  6597  tfrlemibxssdm  6602  tfrlemi14d  6608  tfr1onlembxssdm  6618  tfr1onlemaccex  6623  tfr1onlemres  6624  tfrcllembxssdm  6631  tfrcllemaccex  6636  tfrcllemres  6637  rdgivallem  6656  nnsucelsuc  6768  nnsucsssuc  6769  dcdifsnid  6781  nnawordex  6806  ersym  6823  mapvalg  6936  pmvalg  6937  mapsnd  6975  mapsn  6977  fundmen  7099  1dom1el  7112  en2  7117  pw2f1odclem  7139  mapdom1g  7152  fidceq  7176  fin0or  7195  findcard2  7198  findcard2s  7199  fidcen  7208  prfidceq  7240  fiintim  7243  suplub2ti  7348  supsnti  7352  supisoex  7356  difinfsnlem  7446  difinfsn  7447  ctm  7456  ctssdclemn0  7457  ctssdccl  7458  ctssdc  7460  enumctlemm  7461  nninfninc  7470  nnnninfeq2  7476  enomnilem  7485  exmidomniim  7488  exmidomni  7489  fodjuomnilemdc  7491  fodjuomnilemres  7495  omnimkv  7503  mkvprop  7505  omniwomnimkv  7514  en2prde  7546  pr2cv1  7548  en2eleq  7554  acfun  7570  exmidontriimlem1  7584  exmidontriimlem4  7587  exmidontriim  7588  papsym  7619  papcotr  7620  ccfunen  7637  cc4f  7642  cc4n  7644  elni2  7688  mulclpi  7702  nlt1pig  7715  indpi  7716  recclnq  7766  ltexnqq  7782  halfnqq  7784  prarloclemarch  7792  prarloclemarch2  7793  prop  7849  prltlu  7861  prarloclem3step  7870  prarloclem5  7874  prarloclem  7875  prarloc  7877  prarloc2  7878  genpml  7891  genpmu  7892  genprndl  7895  genprndu  7896  genpdisj  7897  addnqprllem  7901  addnqprulem  7902  addlocprlemeq  7907  addlocprlemgt  7908  addlocprlem  7909  addlocpr  7910  nqprloc  7919  nqprl  7925  nqpru  7926  addnqprlemrl  7931  addnqprlemru  7932  appdivnq  7937  prmuloc  7940  prmuloc2  7941  mullocprlem  7944  mullocpr  7945  mulnqprlemrl  7947  mulnqprlemru  7948  ltprordil  7963  ltpopr  7969  ltsopr  7970  ltaddpr  7971  ltexprlemm  7974  ltexprlemopl  7975  ltexprlemlol  7976  ltexprlemopu  7977  ltexprlemupu  7978  ltexprlemloc  7981  ltexprlemfl  7983  ltexprlemrl  7984  ltexprlemfu  7985  ltexprlemru  7986  ltaprg  7993  recexprlemm  7998  recexprlem1ssl  8007  recexprlem1ssu  8008  aptiprleml  8013  aptiprlemu  8014  archpr  8017  cauappcvgprlemm  8019  cauappcvgprlemopl  8020  cauappcvgprlemlol  8021  cauappcvgprlemopu  8022  cauappcvgprlemupu  8023  cauappcvgprlemdisj  8025  cauappcvgprlemloc  8026  cauappcvgprlemladdfu  8028  cauappcvgprlemladdfl  8029  cauappcvgprlemladdru  8030  cauappcvgprlem1  8033  archrecpr  8038  caucvgprlemnkj  8040  caucvgprlemnbj  8041  caucvgprlemm  8042  caucvgprlemopl  8043  caucvgprlemlol  8044  caucvgprlemopu  8045  caucvgprlemupu  8046  caucvgprlemdisj  8048  caucvgprlemloc  8049  caucvgprlemladdfu  8051  caucvgprlem1  8053  caucvgprlemlim  8055  caucvgprprlemnbj  8067  caucvgprprlemml  8068  caucvgprprlemopl  8071  caucvgprprlemlol  8072  caucvgprprlemopu  8073  caucvgprprlemupu  8074  caucvgprprlemdisj  8076  caucvgprprlemloc  8077  caucvgprprlemexbt  8080  caucvgprprlemaddq  8082  caucvgprprlemlim  8085  suplocexprlemss  8089  suplocexprlemrl  8091  suplocexprlemmu  8092  suplocexprlemru  8093  suplocexprlemdisj  8094  suplocexprlemloc  8095  suplocexprlemub  8097  suplocexprlemlub  8098  recexgt0sr  8147  mulgt0sr  8152  archsr  8156  caucvgsrlemoffcau  8172  suplocsrlemb  8180  suplocsrlempr  8181  suplocsrlem  8182  cnm  8206  axarch  8265  axcaucvglemcau  8272  axpre-suploclemres  8275  lelttr  8421  ltletr  8422  ltled  8453  cnegexlem1  8509  cnegexlem2  8510  renegcl  8595  negf1o  8717  gt0add  8910  apreap  8924  apirr  8942  apsym  8943  apcotr  8944  apadd1  8945  apneg  8948  mulext1  8949  mulap0r  8952  apti  8959  aprcl  8983  aptap  8987  recexap  8990  mulap0  8991  receuap  9008  mul0eqap  9009  lep1  9184  lem1  9186  letrp1  9187  recreclt  9239  lbinf  9287  suprubex  9290  nnrecgt0  9352  bndndx  9574  nn0ge2m1nn  9639  elnn0z  9669  peano2z  9692  zaddcl  9696  ztri3or0  9698  zltnle  9702  zdceq  9732  zdcle  9733  zdclt  9734  zdiv  9746  zeo  9763  fnn0ind  9774  btwnz  9777  uzm1  9970  uzp1  9973  indstr  10010  supinfneg  10012  infsupneg  10013  eluzdc  10027  nn01to3  10034  qapne  10056  xrltled  10219  xrlelttr  10226  xrltletr  10227  ge0nemnf  10244  fzdcel  10462  elfzouz2  10587  fzoss1  10598  fzospliti  10603  elincfzoext  10629  fzocatel  10635  fzostep1  10674  zsupcllemstep  10680  zsupcl  10682  infssuzledc  10685  qtri3or  10693  qltnle  10696  qdceq  10697  qdclt  10698  exbtwnzlemex  10702  rebtwn2zlemstep  10705  rebtwn2z  10707  qbtwnxr  10710  ioom  10713  ico0  10714  ioc0  10715  flqeqceilz  10777  modqadd1  10820  modqmul1  10836  frec2uzuzd  10861  frec2uzlt2d  10863  frec2uzf1od  10865  frecuzrdgrrn  10867  frec2uzrdg  10868  frecuzrdgrcl  10869  frecuzrdgsuc  10873  frecuzrdgrclt  10874  frecuzrdgdomlem  10876  uzsinds  10903  seqvalcd  10920  seqovcd  10926  seq3fveq2  10934  seqfveq2g  10936  seq3shft2  10940  seqshft2g  10941  monoord  10944  seq3split  10947  seqsplitg  10948  seq3caopr3  10950  iseqf1olemab  10961  iseqf1olemnanb  10962  iseqf1olemqk  10966  seqf1oglem1  10978  seqf1og  10980  seq3id3  10983  seq3id2  10985  seq3homo  10986  seqhomog  10989  expgt1  11036  m1expeven  11045  expnbnd  11123  expnlbnd2  11125  nn0ltexp2  11170  apexp1  11179  hashennn  11242  hashfibclem  11305  hashf1lem2  11309  zfz1isolem1  11315  seq3coll  11317  pfxwrdsymbg  11485  wrdind  11517  wrd2ind  11518  cjap  11695  caucvgre  11770  cvg1nlemres  11774  resqrexlemgt0  11809  resqrexlemglsq  11811  resqrexlemga  11812  resqrtcl  11818  abslt  11878  abssubap0  11880  abssubne0  11881  caubnd2  11907  qdenre  11992  maxabslemlub  11997  maxabs  11999  maxleast  12003  fimaxre2  12017  xrmaxiflemlub  12040  xrmaxif  12043  xrmaxltsup  12050  xrmaxadd  12053  xrmineqinf  12061  climuni  12085  2clim  12093  climcn1  12100  climcn2  12101  subcn2  12103  mulcn2  12104  climsqz  12127  climsqz2  12128  climcau  12139  climcvg1nlem  12141  climcaucn  12143  serf0  12144  sumrbdclem  12170  summodclem2  12175  zsumdc  12177  divcnv  12290  absltap  12302  absgtap  12303  mertenslem2  12329  ntrivcvgap  12341  prodrbdclem  12364  prodmodclem2  12370  zproddc  12372  prodssdc  12382  fprodsplitdc  12389  fprodcl2lem  12398  efcllemp  12451  tanvalap  12501  sin01bnd  12550  cos01bnd  12551  sin01gt0  12555  absef  12563  eirrap  12571  dvds0  12599  dvdsmul1  12606  dvdsmultr1d  12625  dvdslelemd  12636  divconjdvds  12642  alzdvds  12647  3dvds  12657  sqoddm1div8z  12679  nno  12699  divalglemex  12715  bits0o  12743  dvdsbnd  12759  dvdslegcd  12767  zeqzmulgcd  12773  gcd0id  12782  gcdaddm  12787  gcd1  12790  gcdabs  12791  bezoutlemnewy  12799  bezoutlemstep  12800  bezoutlemmain  12801  bezoutlemex  12804  bezoutlemzz  12805  bezoutlemaz  12806  bezoutlembz  12807  bezoutlembi  12808  bezoutlemle  12811  bezoutlemsup  12812  mulgcd  12819  gcdzeq  12825  dvdsmulgcd  12828  sqgcd  12832  bezoutr1  12836  nninfctlemfo  12843  algcvga  12855  algfx  12856  eucalglt  12861  eucalg  12863  lcmneg  12878  lcmabs  12880  lcmgcdlem  12881  ncoprmgcdne1b  12893  mulgcddvds  12898  qredeq  12900  divgcdcoprm0  12905  cncongr1  12907  isprm2lem  12920  nprm  12927  dvdsnprmd  12929  prmdvdsfz  12944  isprm5lem  12946  coprm  12949  isprm6  12952  sqrt2irr  12967  pwbdvdslemn  12970  pwbdvdseulemle  12972  nnmaxpwlemdvds  12975  nnmaxpwlemndvds  12976  sqrt2irrap  12986  qnumdencl  12993  nn0sqdcq  13014  sqrtrirr  13015  prmdiv  13043  modprmn0modprm0  13065  prm23lt5  13072  pythagtriplem4  13077  pythagtriplem19  13091  pythagtrip  13092  pclemub  13096  pcpre1  13101  pcpremul  13102  pceulem  13103  pcqcl  13115  pcidlem  13132  pcgcd1  13137  pc2dvds  13139  dvdsprmpweqle  13146  difsqpwdvds  13147  pcadd  13149  pcmpt  13152  expnprm  13162  pockthg  13166  infpnlem2  13169  prmunb  13171  1arith  13176  4sqlem10  13196  4sqlem11  13210  4sqlem12  13211  4sqlem13m  13212  4sqlem17  13216  4sqlem18  13217  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemfrceq  13331  ennnfonelemex  13364  ennnfonelemhom  13365  ennnfonelemrnh  13366  ennnfonelemnn0  13372  ennnfonelemim  13374  exmidunben  13376  ctinfomlemom  13377  ctinfom  13378  ctinf  13380  omctfn  13393  nninfdclemp1  13400  setscomd  13452  imasaddfnlemg  13695  mhmf1o  13837  grpinveu  13903  grpasscan1  13928  dfgrp3mlem  13963  grp1inv  13972  issubg4m  14056  ghmf1o  14138  gsum2d2fi  14275  srgisid  14398  ringadd2  14440  ringinvnzdiv  14463  unitgrp  14533  ringelnzr  14604  lringuplu  14613  subrguss  14654  subrgintm  14661  aprcotr  14707  islmodd  14739  lssclg  14811  lss0cl  14816  lssvneln0  14820  lss1d  14830  lmodindp1  14875  rnglidlmmgm  14943  znidomb  15103  znunit  15104  znrrg  15105  rnasclassa  15148  mvrf1fi  15215  mplsubgfilemcl  15227  mplsubgfileminv  15228  tgcl  15302  neii1  15385  neii2  15387  neiss  15388  tpnei  15398  tgrest  15407  ssrest  15420  icnpimaex  15449  lmcvg  15455  cnpnei  15457  cnptopco  15460  lmff  15487  txcnp  15509  txcn  15513  hmeontr  15551  blssec  15676  mopni3  15722  blsscls2  15731  comet  15737  bdxmet  15739  bdmopn  15742  xmettxlem  15747  xmettx  15748  addcncntoplem  15799  mpomulcn  15804  mulc1cncf  15827  cncfco  15829  cncfmptc  15834  mulcncflem  15845  mulcncf  15846  dedekindeulemlu  15859  dedekindeulemeu  15860  suplociccreex  15862  suplociccex  15863  dedekindicclemlu  15868  dedekindicclemeu  15869  ivthinclemlopn  15874  ivthinclemlr  15875  ivthinclemuopn  15876  ivthinclemur  15877  ivthinclemloc  15879  ivthinc  15881  ivthreinc  15883  ivthdichlem  15889  limcimolemlt  15902  limcresi  15904  cnplimcim  15905  cnplimclemle  15906  cnplimclemr  15907  limccnpcntop  15913  limccoap  15916  dvcoapbr  15945  dvcj  15947  plyf  15975  plyaddlem1  15985  plymullem1  15986  plyco  15997  plycj  15999  plycn  16000  plyrecj  16001  dvply2g  16004  efltlemlt  16012  sin0pilem2  16021  tangtx  16077  logdivlti  16123  logdivlt  16136  rplogbval  16193  logbgcd1irraplemexp  16216  logbgcd1irraplemap  16217  logbgcd1irrap  16218  zprmlogbaplem2  16228  zprmlogbap  16230  birthdaylem1g  16237  ppiublem2  16304  chtublem  16307  chtqub  16308  perfect1  16310  perfectlem1  16311  perfectlem2  16312  bposlem6  16328  bposlem9  16331  bpos  16332  lgsval4a  16358  lgsdir2lem3  16366  lgsne0  16374  gausslemma2dlem3  16399  gausslemma2dlem4  16400  gausslemma2dlem6  16403  gausslemma2dlem7  16404  gausslemma2d  16405  lgseisenlem1  16406  lgsquadlem2  16414  lgsquadlem3  16415  lgsquad2lem2  16418  lgsquad3  16420  2lgsoddprmlem2  16442  2sqlem8a  16458  2sqlem8  16459  2sqlem9  16460  lpvtx  16537  upgrex  16561  upgr1een  16582  edgupgren  16599  umgredg  16603  upgrpredgv  16604  upgredg2vtx  16606  upgredgpr  16607  uspgrf1oedg  16634  usgredg4  16673  uspgredgdomord  16687  usgr1vr  16706  wlkvtxiedg  16803  wlkvtxiedgg  16804  wlk1walkdom  16817  upgriswlkdc  16818  upgrwlkedg  16819  uspgr2wlkeq  16823  uspgr2wlkeqi  16825  umgrwlknloop  16826  eupth2lem2dc  16917  trlsegvdeglem1  16918  eupth2lem3lem4fi  16931  bj-exlimmpi  17015  uzdcinzz  17043  bj-charfundcALT  17052  bj-2inf  17181  bj-peano4  17198  bj-nn0suc  17207  pw1ndom3  17237  subctctexmid  17247  exmidcon  17254  nninfalllem1  17269  nninfsellemqall  17276  nninfomnilem  17279  nninffeq  17281  nnnninfex  17283  exmidsbthrlem  17285  sbthomlem  17288  refeq  17291  isomninnlem  17297  apdifflemr  17315  redcwlpo  17324  reap0  17327  nconstwlpolem  17334