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  623  mt2d  628  mpjaod  722  stdcndcOLD  850  impidc  862  jadc  867  pm2.54dc  895  oplem1  980  mp3and  1355  xor3dc  1409  exlimdd  1898  exlimddv  1925  eqrdav  2208  necon1aidc  2431  necon1bidc  2432  necon4aidc  2448  reximddv  2613  reximssdv  2614  rexlimddv  2633  vtoclgft  2831  rspcedvd  2893  sseldd  3205  ssneldd  3207  tpid3g  3761  preq12b  3827  axpweq  4234  exmid1dc  4263  exmid1stab  4271  opth  4302  issod  4387  frirrg  4418  frind  4420  ralxfr2d  4532  rexxfr2d  4533  eldifpw  4545  onun2  4559  onuni  4563  elirr  4610  en2lp  4623  wetriext  4646  peano2  4664  relop  4849  elres  5017  sotri2  5102  iota4an  5275  iota5  5276  funeu  5319  funopg  5328  imadiflem  5376  funimaexglem  5380  ssimaex  5668  ffvelcdm  5741  dff3im  5753  dffo4  5756  funopsn  5790  f1eqcocnv  5888  f1oiso2  5924  riota5f  5954  riotass2  5956  acexmidlemcase  5969  ovmpodf  6107  ovmpodv2  6109  ovi3  6113  ov6g  6114  caoftrn  6221  op1steq  6295  tfr0dm  6438  tfrlemibxssdm  6443  tfrlemi14d  6449  tfr1onlembxssdm  6459  tfr1onlemaccex  6464  tfr1onlemres  6465  tfrcllembxssdm  6472  tfrcllemaccex  6477  tfrcllemres  6478  rdgivallem  6497  nnsucelsuc  6607  nnsucsssuc  6608  dcdifsnid  6620  nnawordex  6645  ersym  6662  mapvalg  6775  pmvalg  6776  mapsn  6807  fundmen  6929  en2  6943  pw2f1odclem  6963  mapdom1g  6976  fidceq  6999  fin0or  7016  findcard2  7019  findcard2s  7020  prfidceq  7058  fiintim  7061  suplub2ti  7136  supsnti  7140  supisoex  7144  difinfsnlem  7234  difinfsn  7235  ctm  7244  ctssdclemn0  7245  ctssdccl  7246  ctssdc  7248  enumctlemm  7249  nninfninc  7258  nnnninfeq2  7264  enomnilem  7273  exmidomniim  7276  exmidomni  7277  fodjuomnilemdc  7279  fodjuomnilemres  7283  omnimkv  7291  mkvprop  7293  omniwomnimkv  7302  en2prde  7334  pr2cv1  7336  en2eleq  7341  acfun  7357  exmidontriimlem1  7371  exmidontriimlem4  7374  exmidontriim  7375  ccfunen  7418  cc4f  7423  cc4n  7425  elni2  7469  mulclpi  7483  nlt1pig  7496  indpi  7497  recclnq  7547  ltexnqq  7563  halfnqq  7565  prarloclemarch  7573  prarloclemarch2  7574  prop  7630  prltlu  7642  prarloclem3step  7651  prarloclem5  7655  prarloclem  7656  prarloc  7658  prarloc2  7659  genpml  7672  genpmu  7673  genprndl  7676  genprndu  7677  genpdisj  7678  addnqprllem  7682  addnqprulem  7683  addlocprlemeq  7688  addlocprlemgt  7689  addlocprlem  7690  addlocpr  7691  nqprloc  7700  nqprl  7706  nqpru  7707  addnqprlemrl  7712  addnqprlemru  7713  appdivnq  7718  prmuloc  7721  prmuloc2  7722  mullocprlem  7725  mullocpr  7726  mulnqprlemrl  7728  mulnqprlemru  7729  ltprordil  7744  ltpopr  7750  ltsopr  7751  ltaddpr  7752  ltexprlemm  7755  ltexprlemopl  7756  ltexprlemlol  7757  ltexprlemopu  7758  ltexprlemupu  7759  ltexprlemloc  7762  ltexprlemfl  7764  ltexprlemrl  7765  ltexprlemfu  7766  ltexprlemru  7767  ltaprg  7774  recexprlemm  7779  recexprlem1ssl  7788  recexprlem1ssu  7789  aptiprleml  7794  aptiprlemu  7795  archpr  7798  cauappcvgprlemm  7800  cauappcvgprlemopl  7801  cauappcvgprlemlol  7802  cauappcvgprlemopu  7803  cauappcvgprlemupu  7804  cauappcvgprlemdisj  7806  cauappcvgprlemloc  7807  cauappcvgprlemladdfu  7809  cauappcvgprlemladdfl  7810  cauappcvgprlemladdru  7811  cauappcvgprlem1  7814  archrecpr  7819  caucvgprlemnkj  7821  caucvgprlemnbj  7822  caucvgprlemm  7823  caucvgprlemopl  7824  caucvgprlemlol  7825  caucvgprlemopu  7826  caucvgprlemupu  7827  caucvgprlemdisj  7829  caucvgprlemloc  7830  caucvgprlemladdfu  7832  caucvgprlem1  7834  caucvgprlemlim  7836  caucvgprprlemnbj  7848  caucvgprprlemml  7849  caucvgprprlemopl  7852  caucvgprprlemlol  7853  caucvgprprlemopu  7854  caucvgprprlemupu  7855  caucvgprprlemdisj  7857  caucvgprprlemloc  7858  caucvgprprlemexbt  7861  caucvgprprlemaddq  7863  caucvgprprlemlim  7866  suplocexprlemss  7870  suplocexprlemrl  7872  suplocexprlemmu  7873  suplocexprlemru  7874  suplocexprlemdisj  7875  suplocexprlemloc  7876  suplocexprlemub  7878  suplocexprlemlub  7879  recexgt0sr  7928  mulgt0sr  7933  archsr  7937  caucvgsrlemoffcau  7953  suplocsrlemb  7961  suplocsrlempr  7962  suplocsrlem  7963  cnm  7987  axarch  8046  axcaucvglemcau  8053  axpre-suploclemres  8056  lelttr  8203  ltletr  8204  ltled  8233  cnegexlem1  8289  cnegexlem2  8290  renegcl  8375  negf1o  8496  gt0add  8688  apreap  8702  apirr  8720  apsym  8721  apcotr  8722  apadd1  8723  apneg  8726  mulext1  8727  mulap0r  8730  apti  8737  aprcl  8761  aptap  8765  recexap  8768  mulap0  8769  receuap  8784  mul0eqap  8785  lep1  8960  lem1  8962  letrp1  8963  recreclt  9015  lbinf  9063  suprubex  9066  nnrecgt0  9116  bndndx  9336  nn0ge2m1nn  9397  elnn0z  9427  peano2z  9450  zaddcl  9454  ztri3or0  9456  zltnle  9460  zdceq  9490  zdcle  9491  zdclt  9492  zdiv  9503  zeo  9520  fnn0ind  9531  btwnz  9534  uzm1  9721  uzp1  9724  indstr  9756  supinfneg  9758  infsupneg  9759  eluzdc  9773  nn01to3  9780  qapne  9802  xrltled  9963  xrlelttr  9970  xrltletr  9971  ge0nemnf  9988  fzdcel  10204  elfzouz2  10326  fzoss1  10337  fzospliti  10342  elincfzoext  10366  fzocatel  10372  fzostep1  10410  zsupcllemstep  10416  zsupcl  10418  infssuzledc  10421  qtri3or  10427  qltnle  10430  qdceq  10431  qdclt  10432  exbtwnzlemex  10436  rebtwn2zlemstep  10439  rebtwn2z  10441  qbtwnxr  10444  ioom  10447  ico0  10448  ioc0  10449  flqeqceilz  10507  modqadd1  10550  modqmul1  10566  frec2uzuzd  10591  frec2uzlt2d  10593  frec2uzf1od  10595  frecuzrdgrrn  10597  frec2uzrdg  10598  frecuzrdgrcl  10599  frecuzrdgsuc  10603  frecuzrdgrclt  10604  frecuzrdgdomlem  10606  uzsinds  10633  seqvalcd  10650  seqovcd  10656  seq3fveq2  10664  seqfveq2g  10666  seq3shft2  10670  seqshft2g  10671  monoord  10674  seq3split  10677  seqsplitg  10678  seq3caopr3  10680  iseqf1olemab  10691  iseqf1olemnanb  10692  iseqf1olemqk  10696  seqf1oglem1  10708  seqf1og  10710  seq3id3  10713  seq3id2  10715  seq3homo  10716  seqhomog  10719  expgt1  10766  m1expeven  10775  expnbnd  10852  expnlbnd2  10854  nn0ltexp2  10898  apexp1  10907  hashennn  10969  zfz1isolem1  11029  seq3coll  11031  pfxwrdsymbg  11188  wrdind  11220  wrd2ind  11221  cjap  11383  caucvgre  11458  cvg1nlemres  11462  resqrexlemgt0  11497  resqrexlemglsq  11499  resqrexlemga  11500  resqrtcl  11506  abslt  11565  abssubap0  11567  abssubne0  11568  caubnd2  11594  qdenre  11679  maxabslemlub  11684  maxabs  11686  maxleast  11690  fimaxre2  11704  xrmaxiflemlub  11725  xrmaxif  11728  xrmaxltsup  11735  xrmaxadd  11738  xrmineqinf  11746  climuni  11770  2clim  11778  climcn1  11785  climcn2  11786  subcn2  11788  mulcn2  11789  climsqz  11812  climsqz2  11813  climcau  11824  climcvg1nlem  11826  climcaucn  11828  serf0  11829  sumrbdclem  11854  summodclem2  11859  zsumdc  11861  divcnv  11974  absltap  11986  absgtap  11987  mertenslem2  12013  ntrivcvgap  12025  prodrbdclem  12048  prodmodclem2  12054  zproddc  12056  prodssdc  12066  fprodsplitdc  12073  fprodcl2lem  12082  efcllemp  12135  tanvalap  12185  sin01bnd  12234  cos01bnd  12235  sin01gt0  12239  absef  12247  eirrap  12255  dvds0  12283  dvdsmul1  12290  dvdsmultr1d  12309  dvdslelemd  12320  divconjdvds  12326  alzdvds  12331  3dvds  12341  sqoddm1div8z  12363  nno  12383  divalglemex  12399  bits0o  12427  dvdsbnd  12443  dvdslegcd  12451  zeqzmulgcd  12457  gcd0id  12466  gcdaddm  12471  gcd1  12474  gcdabs  12475  bezoutlemnewy  12483  bezoutlemstep  12484  bezoutlemmain  12485  bezoutlemex  12488  bezoutlemzz  12489  bezoutlemaz  12490  bezoutlembz  12491  bezoutlembi  12492  bezoutlemle  12495  bezoutlemsup  12496  mulgcd  12503  gcdzeq  12509  dvdsmulgcd  12512  sqgcd  12516  bezoutr1  12520  nninfctlemfo  12527  algcvga  12539  algfx  12540  eucalglt  12545  eucalg  12547  lcmneg  12562  lcmabs  12564  lcmgcdlem  12565  ncoprmgcdne1b  12577  mulgcddvds  12582  qredeq  12584  divgcdcoprm0  12589  cncongr1  12591  isprm2lem  12604  nprm  12611  dvdsnprmd  12613  prmdvdsfz  12627  isprm5lem  12629  coprm  12632  isprm6  12635  sqrt2irr  12650  pw2dvdslemn  12653  pw2dvdseulemle  12655  oddpwdclemdvds  12658  oddpwdclemndvds  12659  sqrt2irrap  12668  qnumdencl  12675  prmdiv  12723  modprmn0modprm0  12745  prm23lt5  12752  pythagtriplem4  12757  pythagtriplem19  12771  pythagtrip  12772  pclemub  12776  pcpre1  12781  pcpremul  12782  pceulem  12783  pcqcl  12795  pcidlem  12812  pcgcd1  12817  pc2dvds  12819  dvdsprmpweqle  12826  difsqpwdvds  12827  pcadd  12829  pcmpt  12832  expnprm  12842  pockthg  12846  infpnlem2  12849  prmunb  12851  1arith  12856  4sqlem10  12876  4sqlem11  12890  4sqlem12  12891  4sqlem13m  12892  4sqlem17  12896  4sqlem18  12897  ennnfonelemex  12951  ennnfonelemhom  12952  ennnfonelemrnh  12953  ennnfonelemnn0  12959  ennnfonelemim  12961  exmidunben  12963  ctinfomlemom  12964  ctinfom  12965  ctinf  12967  omctfn  12980  nninfdclemp1  12987  setscomd  13039  imasaddfnlemg  13313  mhmf1o  13469  grpinveu  13537  grpasscan1  13562  dfgrp3mlem  13597  grp1inv  13606  issubg4m  13696  ghmf1o  13778  srgisid  13915  ringadd2  13956  ringinvnzdiv  13979  unitgrp  14045  ringelnzr  14116  lringuplu  14125  subrguss  14165  subrgintm  14172  aprcotr  14214  islmodd  14222  lssclg  14293  lss0cl  14298  lssvneln0  14302  lss1d  14312  lmodindp1  14357  rnglidlmmgm  14425  znidomb  14587  znunit  14588  znrrg  14589  mplsubgfilemcl  14628  mplsubgfileminv  14629  tgcl  14703  neii1  14786  neii2  14788  neiss  14789  tpnei  14799  tgrest  14808  ssrest  14821  icnpimaex  14850  lmcvg  14856  cnpnei  14858  cnptopco  14861  lmff  14888  txcnp  14910  txcn  14914  hmeontr  14952  blssec  15077  mopni3  15123  blsscls2  15132  comet  15138  bdxmet  15140  bdmopn  15143  xmettxlem  15148  xmettx  15149  addcncntoplem  15200  mpomulcn  15205  mulc1cncf  15228  cncfco  15230  cncfmptc  15235  mulcncflem  15246  mulcncf  15247  dedekindeulemlu  15260  dedekindeulemeu  15261  suplociccreex  15263  suplociccex  15264  dedekindicclemlu  15269  dedekindicclemeu  15270  ivthinclemlopn  15275  ivthinclemlr  15276  ivthinclemuopn  15277  ivthinclemur  15278  ivthinclemloc  15280  ivthinc  15282  ivthreinc  15284  ivthdichlem  15290  limcimolemlt  15303  limcresi  15305  cnplimcim  15306  cnplimclemle  15307  cnplimclemr  15308  limccnpcntop  15314  limccoap  15317  dvcoapbr  15346  dvcj  15348  plyf  15376  plyaddlem1  15386  plymullem1  15387  plyco  15398  plycj  15400  plycn  15401  plyrecj  15402  dvply2g  15405  efltlemlt  15413  sin0pilem2  15421  tangtx  15477  logdivlti  15520  rplogbval  15584  logbgcd1irraplemexp  15607  logbgcd1irraplemap  15608  logbgcd1irrap  15609  perfect1  15637  perfectlem1  15638  perfectlem2  15639  lgsval4a  15666  lgsdir2lem3  15674  lgsne0  15682  gausslemma2dlem3  15707  gausslemma2dlem4  15708  gausslemma2dlem6  15711  gausslemma2dlem7  15712  gausslemma2d  15713  lgseisenlem1  15714  lgsquadlem2  15722  lgsquadlem3  15723  lgsquad2lem2  15726  lgsquad3  15728  2lgsoddprmlem2  15750  2sqlem8a  15766  2sqlem8  15767  2sqlem9  15768  lpvtx  15844  upgrex  15868  edgupgren  15904  umgredg  15908  upgrpredgv  15909  upgredg2vtx  15911  upgredgpr  15912  uspgrf1oedg  15939  usgredg4  15978  uspgredgdomord  15992  bj-exlimmpi  16044  uzdcinzz  16072  bj-charfundcALT  16082  bj-2inf  16211  bj-peano4  16228  bj-nn0suc  16237  1dom1el  16264  subctctexmid  16277  nninfalllem1  16285  nninfsellemqall  16292  nninfomnilem  16295  nninffeq  16297  nnnninfex  16299  exmidsbthrlem  16301  sbthomlem  16304  refeq  16307  isomninnlem  16309  apdifflemr  16326  redcwlpo  16334  reap0  16337  nconstwlpolem  16344