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  146  mpbird  166  jcai  309  mp2and  430  pm2.21dd  610  mt2d  615  mpjaod  708  stdcndcOLD  836  impidc  848  jadc  853  pm2.54dc  881  pm4.55dc  928  oplem1  965  mp3and  1330  xor3dc  1377  exlimdd  1860  exlimddv  1886  eqrdav  2164  necon1aidc  2386  necon1bidc  2387  necon4aidc  2403  reximddv  2568  reximssdv  2569  rexlimddv  2587  vtoclgft  2775  rspcedvd  2835  sseldd  3142  ssneldd  3144  tpid3g  3690  preq12b  3749  axpweq  4149  exmid1dc  4178  opth  4214  issod  4296  frirrg  4327  frind  4329  ralxfr2d  4441  rexxfr2d  4442  eldifpw  4454  onun2  4466  onuni  4470  elirr  4517  en2lp  4530  wetriext  4553  peano2  4571  relop  4753  elres  4919  sotri2  5000  iota4an  5171  iota5  5172  funeu  5212  funopg  5221  imadiflem  5266  funimaexglem  5270  ssimaex  5546  ffvelrn  5617  dff3im  5629  dffo4  5632  f1eqcocnv  5758  f1oiso2  5794  riota5f  5821  riotass2  5823  acexmidlemcase  5836  ovmpodf  5969  ovmpodv2  5971  ovi3  5974  ov6g  5975  caoftrn  6074  op1steq  6144  tfr0dm  6286  tfrlemibxssdm  6291  tfrlemi14d  6297  tfr1onlembxssdm  6307  tfr1onlemaccex  6312  tfr1onlemres  6313  tfrcllembxssdm  6320  tfrcllemaccex  6325  tfrcllemres  6326  rdgivallem  6345  nnsucelsuc  6455  nnsucsssuc  6456  dcdifsnid  6468  nnawordex  6492  ersym  6509  mapvalg  6620  pmvalg  6621  mapsn  6652  fundmen  6768  mapdom1g  6809  fidceq  6831  fin0or  6848  findcard2  6851  findcard2s  6852  fiintim  6890  suplub2ti  6962  supsnti  6966  supisoex  6970  difinfsnlem  7060  difinfsn  7061  ctm  7070  ctssdclemn0  7071  ctssdccl  7072  ctssdc  7074  enumctlemm  7075  nnnninfeq2  7089  enomnilem  7098  exmidomniim  7101  exmidomni  7102  fodjuomnilemdc  7104  fodjuomnilemres  7108  omnimkv  7116  mkvprop  7118  omniwomnimkv  7127  en2eleq  7147  acfun  7159  exmidontriimlem1  7173  exmidontriimlem4  7176  exmidontriim  7177  ccfunen  7201  cc4f  7206  cc4n  7208  elni2  7251  mulclpi  7265  nlt1pig  7278  indpi  7279  recclnq  7329  ltexnqq  7345  halfnqq  7347  prarloclemarch  7355  prarloclemarch2  7356  prop  7412  prltlu  7424  prarloclem3step  7433  prarloclem5  7437  prarloclem  7438  prarloc  7440  prarloc2  7441  genpml  7454  genpmu  7455  genprndl  7458  genprndu  7459  genpdisj  7460  addnqprllem  7464  addnqprulem  7465  addlocprlemeq  7470  addlocprlemgt  7471  addlocprlem  7472  addlocpr  7473  nqprloc  7482  nqprl  7488  nqpru  7489  addnqprlemrl  7494  addnqprlemru  7495  appdivnq  7500  prmuloc  7503  prmuloc2  7504  mullocprlem  7507  mullocpr  7508  mulnqprlemrl  7510  mulnqprlemru  7511  ltprordil  7526  ltpopr  7532  ltsopr  7533  ltaddpr  7534  ltexprlemm  7537  ltexprlemopl  7538  ltexprlemlol  7539  ltexprlemopu  7540  ltexprlemupu  7541  ltexprlemloc  7544  ltexprlemfl  7546  ltexprlemrl  7547  ltexprlemfu  7548  ltexprlemru  7549  ltaprg  7556  recexprlemm  7561  recexprlem1ssl  7570  recexprlem1ssu  7571  aptiprleml  7576  aptiprlemu  7577  archpr  7580  cauappcvgprlemm  7582  cauappcvgprlemopl  7583  cauappcvgprlemlol  7584  cauappcvgprlemopu  7585  cauappcvgprlemupu  7586  cauappcvgprlemdisj  7588  cauappcvgprlemloc  7589  cauappcvgprlemladdfu  7591  cauappcvgprlemladdfl  7592  cauappcvgprlemladdru  7593  cauappcvgprlem1  7596  archrecpr  7601  caucvgprlemnkj  7603  caucvgprlemnbj  7604  caucvgprlemm  7605  caucvgprlemopl  7606  caucvgprlemlol  7607  caucvgprlemopu  7608  caucvgprlemupu  7609  caucvgprlemdisj  7611  caucvgprlemloc  7612  caucvgprlemladdfu  7614  caucvgprlem1  7616  caucvgprlemlim  7618  caucvgprprlemnbj  7630  caucvgprprlemml  7631  caucvgprprlemopl  7634  caucvgprprlemlol  7635  caucvgprprlemopu  7636  caucvgprprlemupu  7637  caucvgprprlemdisj  7639  caucvgprprlemloc  7640  caucvgprprlemexbt  7643  caucvgprprlemaddq  7645  caucvgprprlemlim  7648  suplocexprlemss  7652  suplocexprlemrl  7654  suplocexprlemmu  7655  suplocexprlemru  7656  suplocexprlemdisj  7657  suplocexprlemloc  7658  suplocexprlemub  7660  suplocexprlemlub  7661  recexgt0sr  7710  mulgt0sr  7715  archsr  7719  caucvgsrlemoffcau  7735  suplocsrlemb  7743  suplocsrlempr  7744  suplocsrlem  7745  cnm  7769  axarch  7828  axcaucvglemcau  7835  axpre-suploclemres  7838  lelttr  7983  ltletr  7984  ltled  8013  cnegexlem1  8069  cnegexlem2  8070  renegcl  8155  negf1o  8276  gt0add  8467  apreap  8481  apirr  8499  apsym  8500  apcotr  8501  apadd1  8502  apneg  8505  mulext1  8506  mulap0r  8509  apti  8516  aprcl  8540  recexap  8546  mulap0  8547  receuap  8562  mul0eqap  8563  lep1  8736  lem1  8738  letrp1  8739  recreclt  8791  lbinf  8839  suprubex  8842  nnrecgt0  8891  bndndx  9109  nn0ge2m1nn  9170  elnn0z  9200  peano2z  9223  zaddcl  9227  ztri3or0  9229  zltnle  9233  zdceq  9262  zdcle  9263  zdclt  9264  zdiv  9275  zeo  9292  fnn0ind  9303  btwnz  9306  uzm1  9492  uzp1  9495  indstr  9527  supinfneg  9529  infsupneg  9530  eluzdc  9544  nn01to3  9551  qapne  9573  xrltled  9731  xrlelttr  9738  xrltletr  9739  ge0nemnf  9756  fzdcel  9971  elfzouz2  10092  fzoss1  10102  fzospliti  10107  fzocatel  10130  fzostep1  10168  qtri3or  10174  qltnle  10177  qdceq  10178  exbtwnzlemex  10181  rebtwn2zlemstep  10184  rebtwn2z  10186  qbtwnxr  10189  ioom  10192  ico0  10193  ioc0  10194  flqeqceilz  10249  modqadd1  10292  modqmul1  10308  frec2uzuzd  10333  frec2uzlt2d  10335  frec2uzf1od  10337  frecuzrdgrrn  10339  frec2uzrdg  10340  frecuzrdgrcl  10341  frecuzrdgsuc  10345  frecuzrdgrclt  10346  frecuzrdgdomlem  10348  uzsinds  10373  seqvalcd  10390  seqovcd  10394  seq3fveq2  10400  seq3shft2  10404  monoord  10407  seq3split  10410  seq3caopr3  10412  iseqf1olemab  10420  iseqf1olemnanb  10421  iseqf1olemqk  10425  seq3id3  10438  seq3id2  10440  seq3homo  10441  expgt1  10489  m1expeven  10498  expnbnd  10574  expnlbnd2  10576  nn0ltexp2  10619  apexp1  10627  hashennn  10689  zfz1isolem1  10749  seq3coll  10751  cjap  10844  caucvgre  10919  cvg1nlemres  10923  resqrexlemgt0  10958  resqrexlemglsq  10960  resqrexlemga  10961  resqrtcl  10967  abslt  11026  abssubap0  11028  abssubne0  11029  caubnd2  11055  qdenre  11140  maxabslemlub  11145  maxabs  11147  maxleast  11151  fimaxre2  11164  xrmaxiflemlub  11185  xrmaxif  11188  xrmaxltsup  11195  xrmaxadd  11198  xrmineqinf  11206  climuni  11230  2clim  11238  climcn1  11245  climcn2  11246  subcn2  11248  mulcn2  11249  climsqz  11272  climsqz2  11273  climcau  11284  climcvg1nlem  11286  climcaucn  11288  serf0  11289  sumrbdclem  11314  summodclem2  11319  zsumdc  11321  divcnv  11434  absltap  11446  absgtap  11447  mertenslem2  11473  ntrivcvgap  11485  prodrbdclem  11508  prodmodclem2  11514  zproddc  11516  prodssdc  11526  fprodsplitdc  11533  fprodcl2lem  11542  efcllemp  11595  tanvalap  11645  sin01bnd  11694  cos01bnd  11695  sin01gt0  11698  absef  11706  eirrap  11714  dvds0  11742  dvdsmul1  11749  dvdsmultr1d  11768  dvdslelemd  11777  divconjdvds  11783  alzdvds  11788  sqoddm1div8z  11819  nno  11839  divalglemex  11855  zsupcllemstep  11874  zsupcl  11876  infssuzledc  11879  dvdsbnd  11885  dvdslegcd  11893  zeqzmulgcd  11899  gcd0id  11908  gcdaddm  11913  gcd1  11916  gcdabs  11917  bezoutlemnewy  11925  bezoutlemstep  11926  bezoutlemmain  11927  bezoutlemex  11930  bezoutlemzz  11931  bezoutlemaz  11932  bezoutlembz  11933  bezoutlembi  11934  bezoutlemle  11937  bezoutlemsup  11938  mulgcd  11945  gcdzeq  11951  dvdsmulgcd  11954  sqgcd  11958  bezoutr1  11962  algcvga  11979  algfx  11980  eucalglt  11985  eucalg  11987  lcmneg  12002  lcmabs  12004  lcmgcdlem  12005  ncoprmgcdne1b  12017  mulgcddvds  12022  qredeq  12024  divgcdcoprm0  12029  cncongr1  12031  isprm2lem  12044  nprm  12051  dvdsnprmd  12053  prmdvdsfz  12067  isprm5lem  12069  coprm  12072  isprm6  12075  sqrt2irr  12090  pw2dvdslemn  12093  pw2dvdseulemle  12095  oddpwdclemdvds  12098  oddpwdclemndvds  12099  sqrt2irrap  12108  qnumdencl  12115  prmdiv  12163  modprmn0modprm0  12184  prm23lt5  12191  pythagtriplem4  12196  pythagtriplem19  12210  pythagtrip  12211  pclemub  12215  pcpre1  12220  pcpremul  12221  pceulem  12222  pcqcl  12234  pcidlem  12250  pcgcd1  12255  pc2dvds  12257  dvdsprmpweqle  12264  difsqpwdvds  12265  pcadd  12267  pcmpt  12269  expnprm  12279  pockthg  12283  infpnlem2  12286  prmunb  12288  1arith  12293  4sqlem10  12313  ennnfonelemex  12343  ennnfonelemhom  12344  ennnfonelemrnh  12345  ennnfonelemnn0  12351  ennnfonelemim  12353  exmidunben  12355  ctinfomlemom  12356  ctinfom  12357  ctinf  12359  omctfn  12372  nninfdclemp1  12379  tgcl  12664  neii1  12747  neii2  12749  neiss  12750  tpnei  12760  tgrest  12769  ssrest  12782  icnpimaex  12811  lmcvg  12817  cnpnei  12819  cnptopco  12822  lmff  12849  txcnp  12871  txcn  12875  hmeontr  12913  blssec  13038  mopni3  13084  blsscls2  13093  comet  13099  bdxmet  13101  bdmopn  13104  xmettxlem  13109  xmettx  13110  addcncntoplem  13151  mulc1cncf  13176  cncfco  13178  cncfmptc  13182  mulcncflem  13190  mulcncf  13191  dedekindeulemlu  13199  dedekindeulemeu  13200  suplociccreex  13202  suplociccex  13203  dedekindicclemlu  13208  dedekindicclemeu  13209  ivthinclemlopn  13214  ivthinclemlr  13215  ivthinclemuopn  13216  ivthinclemur  13217  ivthinclemloc  13219  ivthinc  13221  limcimolemlt  13233  limcresi  13235  cnplimcim  13236  cnplimclemle  13237  cnplimclemr  13238  limccnpcntop  13244  limccoap  13247  dvcoapbr  13271  dvcj  13273  efltlemlt  13295  sin0pilem2  13303  tangtx  13359  logdivlti  13402  rplogbval  13463  logbgcd1irraplemexp  13486  logbgcd1irraplemap  13487  logbgcd1irrap  13488  lgsval4a  13523  lgsdir2lem3  13531  lgsne0  13539  2sqlem8a  13558  2sqlem8  13559  2sqlem9  13560  bj-exlimmpi  13611  uzdcinzz  13639  bj-charfundcALT  13651  bj-2inf  13780  bj-peano4  13797  bj-nn0suc  13806  exmid1stab  13840  subctctexmid  13841  nninfalllem1  13848  nninfsellemqall  13855  nninfomnilem  13858  nninffeq  13860  exmidsbthrlem  13861  sbthomlem  13864  refeq  13867  isomninnlem  13869  apdifflemr  13886  redcwlpo  13894  reap0  13897  nconstwlpolem  13903