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  625  mt2d  630  mpnanrd  699  mpjaod  725  stdcndcOLD  853  impidc  865  jadc  870  pm2.54dc  898  oplem1  983  mp3and  1376  xor3dc  1431  exlimdd  1920  exlimddv  1947  eqrdav  2230  necon1aidc  2453  necon1bidc  2454  necon4aidc  2470  reximddv  2635  reximssdv  2636  rexlimddv  2655  vtoclgft  2854  rspcedvd  2916  sseldd  3228  ssneldd  3230  tpid3g  3787  preq12b  3853  axpweq  4261  exmid1dc  4290  exmid1stab  4298  opth  4329  issod  4416  frirrg  4447  frind  4449  ralxfr2d  4561  rexxfr2d  4562  eldifpw  4574  onun2  4588  onuni  4592  elirr  4639  en2lp  4652  wetriext  4675  peano2  4693  relop  4880  elres  5049  sotri2  5134  iota4an  5307  iota5  5308  funeu  5351  funopg  5360  imadiflem  5409  funimaexglem  5413  ssimaex  5707  ffvelcdm  5780  dff3im  5792  dffo4  5795  funopsn  5830  f1eqcocnv  5932  f1oiso2  5968  riota5f  5998  riotass2  6000  acexmidlemcase  6013  elovimad  6062  ovmpodf  6153  ovmpodv2  6155  ovi3  6159  ov6g  6160  caoftrn  6268  op1steq  6342  tfr0dm  6488  tfrlemibxssdm  6493  tfrlemi14d  6499  tfr1onlembxssdm  6509  tfr1onlemaccex  6514  tfr1onlemres  6515  tfrcllembxssdm  6522  tfrcllemaccex  6527  tfrcllemres  6528  rdgivallem  6547  nnsucelsuc  6659  nnsucsssuc  6660  dcdifsnid  6672  nnawordex  6697  ersym  6714  mapvalg  6827  pmvalg  6828  mapsn  6859  fundmen  6981  1dom1el  6993  en2  6998  pw2f1odclem  7020  mapdom1g  7033  fidceq  7056  fin0or  7075  findcard2  7078  findcard2s  7079  fidcen  7088  prfidceq  7120  fiintim  7123  suplub2ti  7200  supsnti  7204  supisoex  7208  difinfsnlem  7298  difinfsn  7299  ctm  7308  ctssdclemn0  7309  ctssdccl  7310  ctssdc  7312  enumctlemm  7313  nninfninc  7322  nnnninfeq2  7328  enomnilem  7337  exmidomniim  7340  exmidomni  7341  fodjuomnilemdc  7343  fodjuomnilemres  7347  omnimkv  7355  mkvprop  7357  omniwomnimkv  7366  en2prde  7398  pr2cv1  7400  en2eleq  7406  acfun  7422  exmidontriimlem1  7436  exmidontriimlem4  7439  exmidontriim  7440  ccfunen  7483  cc4f  7488  cc4n  7490  elni2  7534  mulclpi  7548  nlt1pig  7561  indpi  7562  recclnq  7612  ltexnqq  7628  halfnqq  7630  prarloclemarch  7638  prarloclemarch2  7639  prop  7695  prltlu  7707  prarloclem3step  7716  prarloclem5  7720  prarloclem  7721  prarloc  7723  prarloc2  7724  genpml  7737  genpmu  7738  genprndl  7741  genprndu  7742  genpdisj  7743  addnqprllem  7747  addnqprulem  7748  addlocprlemeq  7753  addlocprlemgt  7754  addlocprlem  7755  addlocpr  7756  nqprloc  7765  nqprl  7771  nqpru  7772  addnqprlemrl  7777  addnqprlemru  7778  appdivnq  7783  prmuloc  7786  prmuloc2  7787  mullocprlem  7790  mullocpr  7791  mulnqprlemrl  7793  mulnqprlemru  7794  ltprordil  7809  ltpopr  7815  ltsopr  7816  ltaddpr  7817  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemlol  7822  ltexprlemopu  7823  ltexprlemupu  7824  ltexprlemloc  7827  ltexprlemfl  7829  ltexprlemrl  7830  ltexprlemfu  7831  ltexprlemru  7832  ltaprg  7839  recexprlemm  7844  recexprlem1ssl  7853  recexprlem1ssu  7854  aptiprleml  7859  aptiprlemu  7860  archpr  7863  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemupu  7869  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlemladdru  7876  cauappcvgprlem1  7879  archrecpr  7884  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemupu  7892  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemladdfu  7897  caucvgprlem1  7899  caucvgprlemlim  7901  caucvgprprlemnbj  7913  caucvgprprlemml  7914  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemupu  7920  caucvgprprlemdisj  7922  caucvgprprlemloc  7923  caucvgprprlemexbt  7926  caucvgprprlemaddq  7928  caucvgprprlemlim  7931  suplocexprlemss  7935  suplocexprlemrl  7937  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  suplocexprlemlub  7944  recexgt0sr  7993  mulgt0sr  7998  archsr  8002  caucvgsrlemoffcau  8018  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  cnm  8052  axarch  8111  axcaucvglemcau  8118  axpre-suploclemres  8121  lelttr  8268  ltletr  8269  ltled  8298  cnegexlem1  8354  cnegexlem2  8355  renegcl  8440  negf1o  8561  gt0add  8753  apreap  8767  apirr  8785  apsym  8786  apcotr  8787  apadd1  8788  apneg  8791  mulext1  8792  mulap0r  8795  apti  8802  aprcl  8826  aptap  8830  recexap  8833  mulap0  8834  receuap  8849  mul0eqap  8850  lep1  9025  lem1  9027  letrp1  9028  recreclt  9080  lbinf  9128  suprubex  9131  nnrecgt0  9181  bndndx  9401  nn0ge2m1nn  9462  elnn0z  9492  peano2z  9515  zaddcl  9519  ztri3or0  9521  zltnle  9525  zdceq  9555  zdcle  9556  zdclt  9557  zdiv  9568  zeo  9585  fnn0ind  9596  btwnz  9599  uzm1  9787  uzp1  9790  indstr  9827  supinfneg  9829  infsupneg  9830  eluzdc  9844  nn01to3  9851  qapne  9873  xrltled  10034  xrlelttr  10041  xrltletr  10042  ge0nemnf  10059  fzdcel  10275  elfzouz2  10397  fzoss1  10408  fzospliti  10413  elincfzoext  10439  fzocatel  10445  fzostep1  10484  zsupcllemstep  10490  zsupcl  10492  infssuzledc  10495  qtri3or  10501  qltnle  10504  qdceq  10505  qdclt  10506  exbtwnzlemex  10510  rebtwn2zlemstep  10513  rebtwn2z  10515  qbtwnxr  10518  ioom  10521  ico0  10522  ioc0  10523  flqeqceilz  10581  modqadd1  10624  modqmul1  10640  frec2uzuzd  10665  frec2uzlt2d  10667  frec2uzf1od  10669  frecuzrdgrrn  10671  frec2uzrdg  10672  frecuzrdgrcl  10673  frecuzrdgsuc  10677  frecuzrdgrclt  10678  frecuzrdgdomlem  10680  uzsinds  10707  seqvalcd  10724  seqovcd  10730  seq3fveq2  10738  seqfveq2g  10740  seq3shft2  10744  seqshft2g  10745  monoord  10748  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  iseqf1olemab  10765  iseqf1olemnanb  10766  iseqf1olemqk  10770  seqf1oglem1  10782  seqf1og  10784  seq3id3  10787  seq3id2  10789  seq3homo  10790  seqhomog  10793  expgt1  10840  m1expeven  10849  expnbnd  10926  expnlbnd2  10928  nn0ltexp2  10972  apexp1  10981  hashennn  11043  zfz1isolem1  11105  seq3coll  11107  pfxwrdsymbg  11275  wrdind  11307  wrd2ind  11308  cjap  11471  caucvgre  11546  cvg1nlemres  11550  resqrexlemgt0  11585  resqrexlemglsq  11587  resqrexlemga  11588  resqrtcl  11594  abslt  11653  abssubap0  11655  abssubne0  11656  caubnd2  11682  qdenre  11767  maxabslemlub  11772  maxabs  11774  maxleast  11778  fimaxre2  11792  xrmaxiflemlub  11813  xrmaxif  11816  xrmaxltsup  11823  xrmaxadd  11826  xrmineqinf  11834  climuni  11858  2clim  11866  climcn1  11873  climcn2  11874  subcn2  11876  mulcn2  11877  climsqz  11900  climsqz2  11901  climcau  11912  climcvg1nlem  11914  climcaucn  11916  serf0  11917  sumrbdclem  11943  summodclem2  11948  zsumdc  11950  divcnv  12063  absltap  12075  absgtap  12076  mertenslem2  12102  ntrivcvgap  12114  prodrbdclem  12137  prodmodclem2  12143  zproddc  12145  prodssdc  12155  fprodsplitdc  12162  fprodcl2lem  12171  efcllemp  12224  tanvalap  12274  sin01bnd  12323  cos01bnd  12324  sin01gt0  12328  absef  12336  eirrap  12344  dvds0  12372  dvdsmul1  12379  dvdsmultr1d  12398  dvdslelemd  12409  divconjdvds  12415  alzdvds  12420  3dvds  12430  sqoddm1div8z  12452  nno  12472  divalglemex  12488  bits0o  12516  dvdsbnd  12532  dvdslegcd  12540  zeqzmulgcd  12546  gcd0id  12555  gcdaddm  12560  gcd1  12563  gcdabs  12564  bezoutlemnewy  12572  bezoutlemstep  12573  bezoutlemmain  12574  bezoutlemex  12577  bezoutlemzz  12578  bezoutlemaz  12579  bezoutlembz  12580  bezoutlembi  12581  bezoutlemle  12584  bezoutlemsup  12585  mulgcd  12592  gcdzeq  12598  dvdsmulgcd  12601  sqgcd  12605  bezoutr1  12609  nninfctlemfo  12616  algcvga  12628  algfx  12629  eucalglt  12634  eucalg  12636  lcmneg  12651  lcmabs  12653  lcmgcdlem  12654  ncoprmgcdne1b  12666  mulgcddvds  12671  qredeq  12673  divgcdcoprm0  12678  cncongr1  12680  isprm2lem  12693  nprm  12700  dvdsnprmd  12702  prmdvdsfz  12716  isprm5lem  12718  coprm  12721  isprm6  12724  sqrt2irr  12739  pw2dvdslemn  12742  pw2dvdseulemle  12744  oddpwdclemdvds  12747  oddpwdclemndvds  12748  sqrt2irrap  12757  qnumdencl  12764  prmdiv  12812  modprmn0modprm0  12834  prm23lt5  12841  pythagtriplem4  12846  pythagtriplem19  12860  pythagtrip  12861  pclemub  12865  pcpre1  12870  pcpremul  12871  pceulem  12872  pcqcl  12884  pcidlem  12901  pcgcd1  12906  pc2dvds  12908  dvdsprmpweqle  12915  difsqpwdvds  12916  pcadd  12918  pcmpt  12921  expnprm  12931  pockthg  12935  infpnlem2  12938  prmunb  12940  1arith  12945  4sqlem10  12965  4sqlem11  12979  4sqlem12  12980  4sqlem13m  12981  4sqlem17  12985  4sqlem18  12986  ennnfonelemex  13040  ennnfonelemhom  13041  ennnfonelemrnh  13042  ennnfonelemnn0  13048  ennnfonelemim  13050  exmidunben  13052  ctinfomlemom  13053  ctinfom  13054  ctinf  13056  omctfn  13069  nninfdclemp1  13076  setscomd  13128  imasaddfnlemg  13402  mhmf1o  13558  grpinveu  13626  grpasscan1  13651  dfgrp3mlem  13686  grp1inv  13695  issubg4m  13785  ghmf1o  13867  srgisid  14005  ringadd2  14046  ringinvnzdiv  14069  unitgrp  14136  ringelnzr  14207  lringuplu  14216  subrguss  14256  subrgintm  14263  aprcotr  14305  islmodd  14313  lssclg  14384  lss0cl  14389  lssvneln0  14393  lss1d  14403  lmodindp1  14448  rnglidlmmgm  14516  znidomb  14678  znunit  14679  znrrg  14680  mplsubgfilemcl  14719  mplsubgfileminv  14720  tgcl  14794  neii1  14877  neii2  14879  neiss  14880  tpnei  14890  tgrest  14899  ssrest  14912  icnpimaex  14941  lmcvg  14947  cnpnei  14949  cnptopco  14952  lmff  14979  txcnp  15001  txcn  15005  hmeontr  15043  blssec  15168  mopni3  15214  blsscls2  15223  comet  15229  bdxmet  15231  bdmopn  15234  xmettxlem  15239  xmettx  15240  addcncntoplem  15291  mpomulcn  15296  mulc1cncf  15319  cncfco  15321  cncfmptc  15326  mulcncflem  15337  mulcncf  15338  dedekindeulemlu  15351  dedekindeulemeu  15352  suplociccreex  15354  suplociccex  15355  dedekindicclemlu  15360  dedekindicclemeu  15361  ivthinclemlopn  15366  ivthinclemlr  15367  ivthinclemuopn  15368  ivthinclemur  15369  ivthinclemloc  15371  ivthinc  15373  ivthreinc  15375  ivthdichlem  15381  limcimolemlt  15394  limcresi  15396  cnplimcim  15397  cnplimclemle  15398  cnplimclemr  15399  limccnpcntop  15405  limccoap  15408  dvcoapbr  15437  dvcj  15439  plyf  15467  plyaddlem1  15477  plymullem1  15478  plyco  15489  plycj  15491  plycn  15492  plyrecj  15493  dvply2g  15496  efltlemlt  15504  sin0pilem2  15512  tangtx  15568  logdivlti  15611  rplogbval  15675  logbgcd1irraplemexp  15698  logbgcd1irraplemap  15699  logbgcd1irrap  15700  perfect1  15728  perfectlem1  15729  perfectlem2  15730  lgsval4a  15757  lgsdir2lem3  15765  lgsne0  15773  gausslemma2dlem3  15798  gausslemma2dlem4  15799  gausslemma2dlem6  15802  gausslemma2dlem7  15803  gausslemma2d  15804  lgseisenlem1  15805  lgsquadlem2  15813  lgsquadlem3  15814  lgsquad2lem2  15817  lgsquad3  15819  2lgsoddprmlem2  15841  2sqlem8a  15857  2sqlem8  15858  2sqlem9  15859  lpvtx  15936  upgrex  15960  upgr1een  15981  edgupgren  15998  umgredg  16002  upgrpredgv  16003  upgredg2vtx  16005  upgredgpr  16006  uspgrf1oedg  16033  usgredg4  16072  uspgredgdomord  16086  usgr1vr  16105  wlkvtxiedg  16202  wlkvtxiedgg  16203  wlk1walkdom  16216  upgriswlkdc  16217  upgrwlkedg  16218  uspgr2wlkeq  16222  uspgr2wlkeqi  16224  umgrwlknloop  16225  eupth2lem2dc  16316  trlsegvdeglem1  16317  eupth2lem3lem4fi  16330  bj-exlimmpi  16392  uzdcinzz  16420  bj-charfundcALT  16430  bj-2inf  16559  bj-peano4  16576  bj-nn0suc  16585  pw1ndom3  16615  subctctexmid  16627  nninfalllem1  16636  nninfsellemqall  16643  nninfomnilem  16646  nninffeq  16648  nnnninfex  16650  exmidsbthrlem  16652  sbthomlem  16655  refeq  16658  isomninnlem  16660  apdifflemr  16677  redcwlpo  16685  reap0  16688  nconstwlpolem  16695