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  oplem1  977  mp3and  1351  xor3dc  1398  exlimdd  1886  exlimddv  1913  eqrdav  2195  necon1aidc  2418  necon1bidc  2419  necon4aidc  2435  reximddv  2600  reximssdv  2601  rexlimddv  2619  vtoclgft  2814  rspcedvd  2874  sseldd  3185  ssneldd  3187  tpid3g  3738  preq12b  3801  axpweq  4205  exmid1dc  4234  exmid1stab  4242  opth  4271  issod  4355  frirrg  4386  frind  4388  ralxfr2d  4500  rexxfr2d  4501  eldifpw  4513  onun2  4527  onuni  4531  elirr  4578  en2lp  4591  wetriext  4614  peano2  4632  relop  4817  elres  4983  sotri2  5068  iota4an  5240  iota5  5241  funeu  5284  funopg  5293  imadiflem  5338  funimaexglem  5342  ssimaex  5625  ffvelcdm  5698  dff3im  5710  dffo4  5713  f1eqcocnv  5841  f1oiso2  5877  riota5f  5905  riotass2  5907  acexmidlemcase  5920  ovmpodf  6058  ovmpodv2  6060  ovi3  6064  ov6g  6065  caoftrn  6172  op1steq  6246  tfr0dm  6389  tfrlemibxssdm  6394  tfrlemi14d  6400  tfr1onlembxssdm  6410  tfr1onlemaccex  6415  tfr1onlemres  6416  tfrcllembxssdm  6423  tfrcllemaccex  6428  tfrcllemres  6429  rdgivallem  6448  nnsucelsuc  6558  nnsucsssuc  6559  dcdifsnid  6571  nnawordex  6596  ersym  6613  mapvalg  6726  pmvalg  6727  mapsn  6758  fundmen  6874  pw2f1odclem  6904  mapdom1g  6917  fidceq  6939  fin0or  6956  findcard2  6959  findcard2s  6960  prfidceq  6998  fiintim  7001  suplub2ti  7076  supsnti  7080  supisoex  7084  difinfsnlem  7174  difinfsn  7175  ctm  7184  ctssdclemn0  7185  ctssdccl  7186  ctssdc  7188  enumctlemm  7189  nninfninc  7198  nnnninfeq2  7204  enomnilem  7213  exmidomniim  7216  exmidomni  7217  fodjuomnilemdc  7219  fodjuomnilemres  7223  omnimkv  7231  mkvprop  7233  omniwomnimkv  7242  en2eleq  7276  acfun  7292  exmidontriimlem1  7306  exmidontriimlem4  7309  exmidontriim  7310  ccfunen  7349  cc4f  7354  cc4n  7356  elni2  7400  mulclpi  7414  nlt1pig  7427  indpi  7428  recclnq  7478  ltexnqq  7494  halfnqq  7496  prarloclemarch  7504  prarloclemarch2  7505  prop  7561  prltlu  7573  prarloclem3step  7582  prarloclem5  7586  prarloclem  7587  prarloc  7589  prarloc2  7590  genpml  7603  genpmu  7604  genprndl  7607  genprndu  7608  genpdisj  7609  addnqprllem  7613  addnqprulem  7614  addlocprlemeq  7619  addlocprlemgt  7620  addlocprlem  7621  addlocpr  7622  nqprloc  7631  nqprl  7637  nqpru  7638  addnqprlemrl  7643  addnqprlemru  7644  appdivnq  7649  prmuloc  7652  prmuloc2  7653  mullocprlem  7656  mullocpr  7657  mulnqprlemrl  7659  mulnqprlemru  7660  ltprordil  7675  ltpopr  7681  ltsopr  7682  ltaddpr  7683  ltexprlemm  7686  ltexprlemopl  7687  ltexprlemlol  7688  ltexprlemopu  7689  ltexprlemupu  7690  ltexprlemloc  7693  ltexprlemfl  7695  ltexprlemrl  7696  ltexprlemfu  7697  ltexprlemru  7698  ltaprg  7705  recexprlemm  7710  recexprlem1ssl  7719  recexprlem1ssu  7720  aptiprleml  7725  aptiprlemu  7726  archpr  7729  cauappcvgprlemm  7731  cauappcvgprlemopl  7732  cauappcvgprlemlol  7733  cauappcvgprlemopu  7734  cauappcvgprlemupu  7735  cauappcvgprlemdisj  7737  cauappcvgprlemloc  7738  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  cauappcvgprlemladdru  7742  cauappcvgprlem1  7745  archrecpr  7750  caucvgprlemnkj  7752  caucvgprlemnbj  7753  caucvgprlemm  7754  caucvgprlemopl  7755  caucvgprlemlol  7756  caucvgprlemopu  7757  caucvgprlemupu  7758  caucvgprlemdisj  7760  caucvgprlemloc  7761  caucvgprlemladdfu  7763  caucvgprlem1  7765  caucvgprlemlim  7767  caucvgprprlemnbj  7779  caucvgprprlemml  7780  caucvgprprlemopl  7783  caucvgprprlemlol  7784  caucvgprprlemopu  7785  caucvgprprlemupu  7786  caucvgprprlemdisj  7788  caucvgprprlemloc  7789  caucvgprprlemexbt  7792  caucvgprprlemaddq  7794  caucvgprprlemlim  7797  suplocexprlemss  7801  suplocexprlemrl  7803  suplocexprlemmu  7804  suplocexprlemru  7805  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemub  7809  suplocexprlemlub  7810  recexgt0sr  7859  mulgt0sr  7864  archsr  7868  caucvgsrlemoffcau  7884  suplocsrlemb  7892  suplocsrlempr  7893  suplocsrlem  7894  cnm  7918  axarch  7977  axcaucvglemcau  7984  axpre-suploclemres  7987  lelttr  8134  ltletr  8135  ltled  8164  cnegexlem1  8220  cnegexlem2  8221  renegcl  8306  negf1o  8427  gt0add  8619  apreap  8633  apirr  8651  apsym  8652  apcotr  8653  apadd1  8654  apneg  8657  mulext1  8658  mulap0r  8661  apti  8668  aprcl  8692  aptap  8696  recexap  8699  mulap0  8700  receuap  8715  mul0eqap  8716  lep1  8891  lem1  8893  letrp1  8894  recreclt  8946  lbinf  8994  suprubex  8997  nnrecgt0  9047  bndndx  9267  nn0ge2m1nn  9328  elnn0z  9358  peano2z  9381  zaddcl  9385  ztri3or0  9387  zltnle  9391  zdceq  9420  zdcle  9421  zdclt  9422  zdiv  9433  zeo  9450  fnn0ind  9461  btwnz  9464  uzm1  9651  uzp1  9654  indstr  9686  supinfneg  9688  infsupneg  9689  eluzdc  9703  nn01to3  9710  qapne  9732  xrltled  9893  xrlelttr  9900  xrltletr  9901  ge0nemnf  9918  fzdcel  10134  elfzouz2  10256  fzoss1  10266  fzospliti  10271  fzocatel  10294  fzostep1  10332  zsupcllemstep  10338  zsupcl  10340  infssuzledc  10343  qtri3or  10349  qltnle  10352  qdceq  10353  qdclt  10354  exbtwnzlemex  10358  rebtwn2zlemstep  10361  rebtwn2z  10363  qbtwnxr  10366  ioom  10369  ico0  10370  ioc0  10371  flqeqceilz  10429  modqadd1  10472  modqmul1  10488  frec2uzuzd  10513  frec2uzlt2d  10515  frec2uzf1od  10517  frecuzrdgrrn  10519  frec2uzrdg  10520  frecuzrdgrcl  10521  frecuzrdgsuc  10525  frecuzrdgrclt  10526  frecuzrdgdomlem  10528  uzsinds  10555  seqvalcd  10572  seqovcd  10578  seq3fveq2  10586  seqfveq2g  10588  seq3shft2  10592  seqshft2g  10593  monoord  10596  seq3split  10599  seqsplitg  10600  seq3caopr3  10602  iseqf1olemab  10613  iseqf1olemnanb  10614  iseqf1olemqk  10618  seqf1oglem1  10630  seqf1og  10632  seq3id3  10635  seq3id2  10637  seq3homo  10638  seqhomog  10641  expgt1  10688  m1expeven  10697  expnbnd  10774  expnlbnd2  10776  nn0ltexp2  10820  apexp1  10829  hashennn  10891  zfz1isolem1  10951  seq3coll  10953  cjap  11090  caucvgre  11165  cvg1nlemres  11169  resqrexlemgt0  11204  resqrexlemglsq  11206  resqrexlemga  11207  resqrtcl  11213  abslt  11272  abssubap0  11274  abssubne0  11275  caubnd2  11301  qdenre  11386  maxabslemlub  11391  maxabs  11393  maxleast  11397  fimaxre2  11411  xrmaxiflemlub  11432  xrmaxif  11435  xrmaxltsup  11442  xrmaxadd  11445  xrmineqinf  11453  climuni  11477  2clim  11485  climcn1  11492  climcn2  11493  subcn2  11495  mulcn2  11496  climsqz  11519  climsqz2  11520  climcau  11531  climcvg1nlem  11533  climcaucn  11535  serf0  11536  sumrbdclem  11561  summodclem2  11566  zsumdc  11568  divcnv  11681  absltap  11693  absgtap  11694  mertenslem2  11720  ntrivcvgap  11732  prodrbdclem  11755  prodmodclem2  11761  zproddc  11763  prodssdc  11773  fprodsplitdc  11780  fprodcl2lem  11789  efcllemp  11842  tanvalap  11892  sin01bnd  11941  cos01bnd  11942  sin01gt0  11946  absef  11954  eirrap  11962  dvds0  11990  dvdsmul1  11997  dvdsmultr1d  12016  dvdslelemd  12027  divconjdvds  12033  alzdvds  12038  3dvds  12048  sqoddm1div8z  12070  nno  12090  divalglemex  12106  bits0o  12134  dvdsbnd  12150  dvdslegcd  12158  zeqzmulgcd  12164  gcd0id  12173  gcdaddm  12178  gcd1  12181  gcdabs  12182  bezoutlemnewy  12190  bezoutlemstep  12191  bezoutlemmain  12192  bezoutlemex  12195  bezoutlemzz  12196  bezoutlemaz  12197  bezoutlembz  12198  bezoutlembi  12199  bezoutlemle  12202  bezoutlemsup  12203  mulgcd  12210  gcdzeq  12216  dvdsmulgcd  12219  sqgcd  12223  bezoutr1  12227  nninfctlemfo  12234  algcvga  12246  algfx  12247  eucalglt  12252  eucalg  12254  lcmneg  12269  lcmabs  12271  lcmgcdlem  12272  ncoprmgcdne1b  12284  mulgcddvds  12289  qredeq  12291  divgcdcoprm0  12296  cncongr1  12298  isprm2lem  12311  nprm  12318  dvdsnprmd  12320  prmdvdsfz  12334  isprm5lem  12336  coprm  12339  isprm6  12342  sqrt2irr  12357  pw2dvdslemn  12360  pw2dvdseulemle  12362  oddpwdclemdvds  12365  oddpwdclemndvds  12366  sqrt2irrap  12375  qnumdencl  12382  prmdiv  12430  modprmn0modprm0  12452  prm23lt5  12459  pythagtriplem4  12464  pythagtriplem19  12478  pythagtrip  12479  pclemub  12483  pcpre1  12488  pcpremul  12489  pceulem  12490  pcqcl  12502  pcidlem  12519  pcgcd1  12524  pc2dvds  12526  dvdsprmpweqle  12533  difsqpwdvds  12534  pcadd  12536  pcmpt  12539  expnprm  12549  pockthg  12553  infpnlem2  12556  prmunb  12558  1arith  12563  4sqlem10  12583  4sqlem11  12597  4sqlem12  12598  4sqlem13m  12599  4sqlem17  12603  4sqlem18  12604  ennnfonelemex  12658  ennnfonelemhom  12659  ennnfonelemrnh  12660  ennnfonelemnn0  12666  ennnfonelemim  12668  exmidunben  12670  ctinfomlemom  12671  ctinfom  12672  ctinf  12674  omctfn  12687  nninfdclemp1  12694  setscomd  12746  imasaddfnlemg  13018  mhmf1o  13174  grpinveu  13242  grpasscan1  13267  dfgrp3mlem  13302  grp1inv  13311  issubg4m  13401  ghmf1o  13483  srgisid  13620  ringadd2  13661  ringinvnzdiv  13684  unitgrp  13750  ringelnzr  13821  lringuplu  13830  subrguss  13870  subrgintm  13877  aprcotr  13919  islmodd  13927  lssclg  13998  lss0cl  14003  lssvneln0  14007  lss1d  14017  lmodindp1  14062  rnglidlmmgm  14130  znidomb  14292  znunit  14293  znrrg  14294  tgcl  14386  neii1  14469  neii2  14471  neiss  14472  tpnei  14482  tgrest  14491  ssrest  14504  icnpimaex  14533  lmcvg  14539  cnpnei  14541  cnptopco  14544  lmff  14571  txcnp  14593  txcn  14597  hmeontr  14635  blssec  14760  mopni3  14806  blsscls2  14815  comet  14821  bdxmet  14823  bdmopn  14826  xmettxlem  14831  xmettx  14832  addcncntoplem  14883  mpomulcn  14888  mulc1cncf  14911  cncfco  14913  cncfmptc  14918  mulcncflem  14929  mulcncf  14930  dedekindeulemlu  14943  dedekindeulemeu  14944  suplociccreex  14946  suplociccex  14947  dedekindicclemlu  14952  dedekindicclemeu  14953  ivthinclemlopn  14958  ivthinclemlr  14959  ivthinclemuopn  14960  ivthinclemur  14961  ivthinclemloc  14963  ivthinc  14965  ivthreinc  14967  ivthdichlem  14973  limcimolemlt  14986  limcresi  14988  cnplimcim  14989  cnplimclemle  14990  cnplimclemr  14991  limccnpcntop  14997  limccoap  15000  dvcoapbr  15029  dvcj  15031  plyf  15059  plyaddlem1  15069  plymullem1  15070  plyco  15081  plycj  15083  plycn  15084  plyrecj  15085  dvply2g  15088  efltlemlt  15096  sin0pilem2  15104  tangtx  15160  logdivlti  15203  rplogbval  15267  logbgcd1irraplemexp  15290  logbgcd1irraplemap  15291  logbgcd1irrap  15292  perfect1  15320  perfectlem1  15321  perfectlem2  15322  lgsval4a  15349  lgsdir2lem3  15357  lgsne0  15365  gausslemma2dlem3  15390  gausslemma2dlem4  15391  gausslemma2dlem6  15394  gausslemma2dlem7  15395  gausslemma2d  15396  lgseisenlem1  15397  lgsquadlem2  15405  lgsquadlem3  15406  lgsquad2lem2  15409  lgsquad3  15411  2lgsoddprmlem2  15433  2sqlem8a  15449  2sqlem8  15450  2sqlem9  15451  bj-exlimmpi  15502  uzdcinzz  15530  bj-charfundcALT  15541  bj-2inf  15670  bj-peano4  15687  bj-nn0suc  15696  1dom1el  15723  subctctexmid  15733  nninfalllem1  15741  nninfsellemqall  15748  nninfomnilem  15751  nninffeq  15753  nnnninfex  15755  exmidsbthrlem  15757  sbthomlem  15760  refeq  15763  isomninnlem  15765  apdifflemr  15782  redcwlpo  15790  reap0  15793  nconstwlpolem  15800