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  621  mt2d  626  mpjaod  719  stdcndcOLD  847  impidc  859  jadc  864  pm2.54dc  892  pm4.55dc  939  oplem1  976  mp3and  1350  xor3dc  1397  exlimdd  1882  exlimddv  1908  eqrdav  2186  necon1aidc  2408  necon1bidc  2409  necon4aidc  2425  reximddv  2590  reximssdv  2591  rexlimddv  2609  vtoclgft  2799  rspcedvd  2859  sseldd  3168  ssneldd  3170  tpid3g  3719  preq12b  3782  axpweq  4183  exmid1dc  4212  exmid1stab  4220  opth  4249  issod  4331  frirrg  4362  frind  4364  ralxfr2d  4476  rexxfr2d  4477  eldifpw  4489  onun2  4501  onuni  4505  elirr  4552  en2lp  4565  wetriext  4588  peano2  4606  relop  4789  elres  4955  sotri2  5038  iota4an  5209  iota5  5210  funeu  5253  funopg  5262  imadiflem  5307  funimaexglem  5311  ssimaex  5590  ffvelcdm  5662  dff3im  5674  dffo4  5677  f1eqcocnv  5805  f1oiso2  5841  riota5f  5868  riotass2  5870  acexmidlemcase  5883  ovmpodf  6020  ovmpodv2  6022  ovi3  6025  ov6g  6026  caoftrn  6122  op1steq  6194  tfr0dm  6337  tfrlemibxssdm  6342  tfrlemi14d  6348  tfr1onlembxssdm  6358  tfr1onlemaccex  6363  tfr1onlemres  6364  tfrcllembxssdm  6371  tfrcllemaccex  6376  tfrcllemres  6377  rdgivallem  6396  nnsucelsuc  6506  nnsucsssuc  6507  dcdifsnid  6519  nnawordex  6544  ersym  6561  mapvalg  6672  pmvalg  6673  mapsn  6704  fundmen  6820  mapdom1g  6861  fidceq  6883  fin0or  6900  findcard2  6903  findcard2s  6904  fiintim  6942  suplub2ti  7014  supsnti  7018  supisoex  7022  difinfsnlem  7112  difinfsn  7113  ctm  7122  ctssdclemn0  7123  ctssdccl  7124  ctssdc  7126  enumctlemm  7127  nnnninfeq2  7141  enomnilem  7150  exmidomniim  7153  exmidomni  7154  fodjuomnilemdc  7156  fodjuomnilemres  7160  omnimkv  7168  mkvprop  7170  omniwomnimkv  7179  en2eleq  7208  acfun  7220  exmidontriimlem1  7234  exmidontriimlem4  7237  exmidontriim  7238  ccfunen  7277  cc4f  7282  cc4n  7284  elni2  7327  mulclpi  7341  nlt1pig  7354  indpi  7355  recclnq  7405  ltexnqq  7421  halfnqq  7423  prarloclemarch  7431  prarloclemarch2  7432  prop  7488  prltlu  7500  prarloclem3step  7509  prarloclem5  7513  prarloclem  7514  prarloc  7516  prarloc2  7517  genpml  7530  genpmu  7531  genprndl  7534  genprndu  7535  genpdisj  7536  addnqprllem  7540  addnqprulem  7541  addlocprlemeq  7546  addlocprlemgt  7547  addlocprlem  7548  addlocpr  7549  nqprloc  7558  nqprl  7564  nqpru  7565  addnqprlemrl  7570  addnqprlemru  7571  appdivnq  7576  prmuloc  7579  prmuloc2  7580  mullocprlem  7583  mullocpr  7584  mulnqprlemrl  7586  mulnqprlemru  7587  ltprordil  7602  ltpopr  7608  ltsopr  7609  ltaddpr  7610  ltexprlemm  7613  ltexprlemopl  7614  ltexprlemlol  7615  ltexprlemopu  7616  ltexprlemupu  7617  ltexprlemloc  7620  ltexprlemfl  7622  ltexprlemrl  7623  ltexprlemfu  7624  ltexprlemru  7625  ltaprg  7632  recexprlemm  7637  recexprlem1ssl  7646  recexprlem1ssu  7647  aptiprleml  7652  aptiprlemu  7653  archpr  7656  cauappcvgprlemm  7658  cauappcvgprlemopl  7659  cauappcvgprlemlol  7660  cauappcvgprlemopu  7661  cauappcvgprlemupu  7662  cauappcvgprlemdisj  7664  cauappcvgprlemloc  7665  cauappcvgprlemladdfu  7667  cauappcvgprlemladdfl  7668  cauappcvgprlemladdru  7669  cauappcvgprlem1  7672  archrecpr  7677  caucvgprlemnkj  7679  caucvgprlemnbj  7680  caucvgprlemm  7681  caucvgprlemopl  7682  caucvgprlemlol  7683  caucvgprlemopu  7684  caucvgprlemupu  7685  caucvgprlemdisj  7687  caucvgprlemloc  7688  caucvgprlemladdfu  7690  caucvgprlem1  7692  caucvgprlemlim  7694  caucvgprprlemnbj  7706  caucvgprprlemml  7707  caucvgprprlemopl  7710  caucvgprprlemlol  7711  caucvgprprlemopu  7712  caucvgprprlemupu  7713  caucvgprprlemdisj  7715  caucvgprprlemloc  7716  caucvgprprlemexbt  7719  caucvgprprlemaddq  7721  caucvgprprlemlim  7724  suplocexprlemss  7728  suplocexprlemrl  7730  suplocexprlemmu  7731  suplocexprlemru  7732  suplocexprlemdisj  7733  suplocexprlemloc  7734  suplocexprlemub  7736  suplocexprlemlub  7737  recexgt0sr  7786  mulgt0sr  7791  archsr  7795  caucvgsrlemoffcau  7811  suplocsrlemb  7819  suplocsrlempr  7820  suplocsrlem  7821  cnm  7845  axarch  7904  axcaucvglemcau  7911  axpre-suploclemres  7914  lelttr  8060  ltletr  8061  ltled  8090  cnegexlem1  8146  cnegexlem2  8147  renegcl  8232  negf1o  8353  gt0add  8544  apreap  8558  apirr  8576  apsym  8577  apcotr  8578  apadd1  8579  apneg  8582  mulext1  8583  mulap0r  8586  apti  8593  aprcl  8617  aptap  8621  recexap  8624  mulap0  8625  receuap  8640  mul0eqap  8641  lep1  8816  lem1  8818  letrp1  8819  recreclt  8871  lbinf  8919  suprubex  8922  nnrecgt0  8971  bndndx  9189  nn0ge2m1nn  9250  elnn0z  9280  peano2z  9303  zaddcl  9307  ztri3or0  9309  zltnle  9313  zdceq  9342  zdcle  9343  zdclt  9344  zdiv  9355  zeo  9372  fnn0ind  9383  btwnz  9386  uzm1  9572  uzp1  9575  indstr  9607  supinfneg  9609  infsupneg  9610  eluzdc  9624  nn01to3  9631  qapne  9653  xrltled  9813  xrlelttr  9820  xrltletr  9821  ge0nemnf  9838  fzdcel  10054  elfzouz2  10175  fzoss1  10185  fzospliti  10190  fzocatel  10213  fzostep1  10251  qtri3or  10257  qltnle  10260  qdceq  10261  exbtwnzlemex  10264  rebtwn2zlemstep  10267  rebtwn2z  10269  qbtwnxr  10272  ioom  10275  ico0  10276  ioc0  10277  flqeqceilz  10332  modqadd1  10375  modqmul1  10391  frec2uzuzd  10416  frec2uzlt2d  10418  frec2uzf1od  10420  frecuzrdgrrn  10422  frec2uzrdg  10423  frecuzrdgrcl  10424  frecuzrdgsuc  10428  frecuzrdgrclt  10429  frecuzrdgdomlem  10431  uzsinds  10456  seqvalcd  10473  seqovcd  10477  seq3fveq2  10483  seq3shft2  10487  monoord  10490  seq3split  10493  seq3caopr3  10495  iseqf1olemab  10503  iseqf1olemnanb  10504  iseqf1olemqk  10508  seq3id3  10521  seq3id2  10523  seq3homo  10524  expgt1  10572  m1expeven  10581  expnbnd  10658  expnlbnd2  10660  nn0ltexp2  10703  apexp1  10712  hashennn  10774  zfz1isolem1  10834  seq3coll  10836  cjap  10929  caucvgre  11004  cvg1nlemres  11008  resqrexlemgt0  11043  resqrexlemglsq  11045  resqrexlemga  11046  resqrtcl  11052  abslt  11111  abssubap0  11113  abssubne0  11114  caubnd2  11140  qdenre  11225  maxabslemlub  11230  maxabs  11232  maxleast  11236  fimaxre2  11249  xrmaxiflemlub  11270  xrmaxif  11273  xrmaxltsup  11280  xrmaxadd  11283  xrmineqinf  11291  climuni  11315  2clim  11323  climcn1  11330  climcn2  11331  subcn2  11333  mulcn2  11334  climsqz  11357  climsqz2  11358  climcau  11369  climcvg1nlem  11371  climcaucn  11373  serf0  11374  sumrbdclem  11399  summodclem2  11404  zsumdc  11406  divcnv  11519  absltap  11531  absgtap  11532  mertenslem2  11558  ntrivcvgap  11570  prodrbdclem  11593  prodmodclem2  11599  zproddc  11601  prodssdc  11611  fprodsplitdc  11618  fprodcl2lem  11627  efcllemp  11680  tanvalap  11730  sin01bnd  11779  cos01bnd  11780  sin01gt0  11783  absef  11791  eirrap  11799  dvds0  11827  dvdsmul1  11834  dvdsmultr1d  11853  dvdslelemd  11863  divconjdvds  11869  alzdvds  11874  sqoddm1div8z  11905  nno  11925  divalglemex  11941  zsupcllemstep  11960  zsupcl  11962  infssuzledc  11965  dvdsbnd  11971  dvdslegcd  11979  zeqzmulgcd  11985  gcd0id  11994  gcdaddm  11999  gcd1  12002  gcdabs  12003  bezoutlemnewy  12011  bezoutlemstep  12012  bezoutlemmain  12013  bezoutlemex  12016  bezoutlemzz  12017  bezoutlemaz  12018  bezoutlembz  12019  bezoutlembi  12020  bezoutlemle  12023  bezoutlemsup  12024  mulgcd  12031  gcdzeq  12037  dvdsmulgcd  12040  sqgcd  12044  bezoutr1  12048  algcvga  12065  algfx  12066  eucalglt  12071  eucalg  12073  lcmneg  12088  lcmabs  12090  lcmgcdlem  12091  ncoprmgcdne1b  12103  mulgcddvds  12108  qredeq  12110  divgcdcoprm0  12115  cncongr1  12117  isprm2lem  12130  nprm  12137  dvdsnprmd  12139  prmdvdsfz  12153  isprm5lem  12155  coprm  12158  isprm6  12161  sqrt2irr  12176  pw2dvdslemn  12179  pw2dvdseulemle  12181  oddpwdclemdvds  12184  oddpwdclemndvds  12185  sqrt2irrap  12194  qnumdencl  12201  prmdiv  12249  modprmn0modprm0  12270  prm23lt5  12277  pythagtriplem4  12282  pythagtriplem19  12296  pythagtrip  12297  pclemub  12301  pcpre1  12306  pcpremul  12307  pceulem  12308  pcqcl  12320  pcidlem  12336  pcgcd1  12341  pc2dvds  12343  dvdsprmpweqle  12350  difsqpwdvds  12351  pcadd  12353  pcmpt  12355  expnprm  12365  pockthg  12369  infpnlem2  12372  prmunb  12374  1arith  12379  4sqlem10  12399  ennnfonelemex  12429  ennnfonelemhom  12430  ennnfonelemrnh  12431  ennnfonelemnn0  12437  ennnfonelemim  12439  exmidunben  12441  ctinfomlemom  12442  ctinfom  12443  ctinf  12445  omctfn  12458  nninfdclemp1  12465  setscomd  12517  imasaddfnlemg  12753  mhmf1o  12883  grpinveu  12935  grpasscan1  12960  dfgrp3mlem  12995  grp1inv  13004  issubg4m  13085  srgisid  13238  ringadd2  13279  ringinvnzdiv  13300  unitgrp  13364  ringelnzr  13407  lringuplu  13416  subrguss  13456  subrgintm  13463  aprcotr  13474  islmodd  13482  lssclg  13553  lss0cl  13558  lssvneln0  13562  lss1d  13572  lmodindp1  13617  rnglidlmmgm  13685  tgcl  13860  neii1  13943  neii2  13945  neiss  13946  tpnei  13956  tgrest  13965  ssrest  13978  icnpimaex  14007  lmcvg  14013  cnpnei  14015  cnptopco  14018  lmff  14045  txcnp  14067  txcn  14071  hmeontr  14109  blssec  14234  mopni3  14280  blsscls2  14289  comet  14295  bdxmet  14297  bdmopn  14300  xmettxlem  14305  xmettx  14306  addcncntoplem  14347  mulc1cncf  14372  cncfco  14374  cncfmptc  14378  mulcncflem  14386  mulcncf  14387  dedekindeulemlu  14395  dedekindeulemeu  14396  suplociccreex  14398  suplociccex  14399  dedekindicclemlu  14404  dedekindicclemeu  14405  ivthinclemlopn  14410  ivthinclemlr  14411  ivthinclemuopn  14412  ivthinclemur  14413  ivthinclemloc  14415  ivthinc  14417  limcimolemlt  14429  limcresi  14431  cnplimcim  14432  cnplimclemle  14433  cnplimclemr  14434  limccnpcntop  14440  limccoap  14443  dvcoapbr  14467  dvcj  14469  efltlemlt  14491  sin0pilem2  14499  tangtx  14555  logdivlti  14598  rplogbval  14659  logbgcd1irraplemexp  14682  logbgcd1irraplemap  14683  logbgcd1irrap  14684  lgsval4a  14719  lgsdir2lem3  14727  lgsne0  14735  lgseisenlem1  14746  2lgsoddprmlem2  14750  2sqlem8a  14765  2sqlem8  14766  2sqlem9  14767  bj-exlimmpi  14818  uzdcinzz  14846  bj-charfundcALT  14857  bj-2inf  14986  bj-peano4  15003  bj-nn0suc  15012  1dom1el  15039  subctctexmid  15047  nninfalllem1  15054  nninfsellemqall  15061  nninfomnilem  15064  nninffeq  15066  exmidsbthrlem  15067  sbthomlem  15070  refeq  15073  isomninnlem  15075  apdifflemr  15092  redcwlpo  15100  reap0  15103  nconstwlpolem  15110