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  700  mpjaod  726  stdcndcOLD  854  impidc  866  jadc  871  pm2.54dc  899  oplem1  984  mp3and  1377  xor3dc  1432  exlimdd  1921  exlimddv  1950  eqrdav  2233  necon1aidc  2465  necon1bidc  2466  necon4aidc  2482  reximddv  2647  reximssdv  2648  rexlimddv  2667  vtoclgft  2867  rspcedvd  2929  sseldd  3243  ssneldd  3245  tpid3g  3812  preq12b  3879  axpweq  4289  exmid1dc  4318  exmid1stab  4326  opth  4358  issod  4445  frirrg  4476  frind  4478  ralxfr2d  4590  rexxfr2d  4591  eldifpw  4603  onun2  4617  onuni  4621  elirr  4668  en2lp  4681  wetriext  4704  peano2  4722  relop  4910  elres  5079  sotri2  5165  iota4an  5338  iota5  5339  funeu  5382  funopg  5391  imadiflem  5440  funimaexglem  5444  ssimaex  5743  ffvelcdm  5815  dff3im  5827  dffo4  5830  funopsn  5865  f1eqcocnv  5970  f1oiso2  6006  riota5f  6038  riotass2  6040  acexmidlemcase  6053  elovimad  6102  ovmpodf  6193  ovmpodv2  6195  ovi3  6199  ov6g  6200  caoftrn  6308  op1steq  6386  fvdifsuppst  6457  suppssdc  6473  suppofss1dcl  6477  suppofss2dcl  6478  tfr0dm  6566  tfrlemibxssdm  6571  tfrlemi14d  6577  tfr1onlembxssdm  6587  tfr1onlemaccex  6592  tfr1onlemres  6593  tfrcllembxssdm  6600  tfrcllemaccex  6605  tfrcllemres  6606  rdgivallem  6625  nnsucelsuc  6737  nnsucsssuc  6738  dcdifsnid  6750  nnawordex  6775  ersym  6792  mapvalg  6905  pmvalg  6906  mapsnd  6936  mapsn  6938  fundmen  7060  1dom1el  7073  en2  7078  pw2f1odclem  7100  mapdom1g  7113  fidceq  7137  fin0or  7156  findcard2  7159  findcard2s  7160  fidcen  7169  prfidceq  7201  fiintim  7204  suplub2ti  7305  supsnti  7309  supisoex  7313  difinfsnlem  7403  difinfsn  7404  ctm  7413  ctssdclemn0  7414  ctssdccl  7415  ctssdc  7417  enumctlemm  7418  nninfninc  7427  nnnninfeq2  7433  enomnilem  7442  exmidomniim  7445  exmidomni  7446  fodjuomnilemdc  7448  fodjuomnilemres  7452  omnimkv  7460  mkvprop  7462  omniwomnimkv  7471  en2prde  7503  pr2cv1  7505  en2eleq  7511  acfun  7527  exmidontriimlem1  7541  exmidontriimlem4  7544  exmidontriim  7545  papsym  7576  papcotr  7577  ccfunen  7594  cc4f  7599  cc4n  7601  elni2  7645  mulclpi  7659  nlt1pig  7672  indpi  7673  recclnq  7723  ltexnqq  7739  halfnqq  7741  prarloclemarch  7749  prarloclemarch2  7750  prop  7806  prltlu  7818  prarloclem3step  7827  prarloclem5  7831  prarloclem  7832  prarloc  7834  prarloc2  7835  genpml  7848  genpmu  7849  genprndl  7852  genprndu  7853  genpdisj  7854  addnqprllem  7858  addnqprulem  7859  addlocprlemeq  7864  addlocprlemgt  7865  addlocprlem  7866  addlocpr  7867  nqprloc  7876  nqprl  7882  nqpru  7883  addnqprlemrl  7888  addnqprlemru  7889  appdivnq  7894  prmuloc  7897  prmuloc2  7898  mullocprlem  7901  mullocpr  7902  mulnqprlemrl  7904  mulnqprlemru  7905  ltprordil  7920  ltpopr  7926  ltsopr  7927  ltaddpr  7928  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemlol  7933  ltexprlemopu  7934  ltexprlemupu  7935  ltexprlemloc  7938  ltexprlemfl  7940  ltexprlemrl  7941  ltexprlemfu  7942  ltexprlemru  7943  ltaprg  7950  recexprlemm  7955  recexprlem1ssl  7964  recexprlem1ssu  7965  aptiprleml  7970  aptiprlemu  7971  archpr  7974  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemupu  7980  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlemladdru  7987  cauappcvgprlem1  7990  archrecpr  7995  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemupu  8003  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemladdfu  8008  caucvgprlem1  8010  caucvgprlemlim  8012  caucvgprprlemnbj  8024  caucvgprprlemml  8025  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemupu  8031  caucvgprprlemdisj  8033  caucvgprprlemloc  8034  caucvgprprlemexbt  8037  caucvgprprlemaddq  8039  caucvgprprlemlim  8042  suplocexprlemss  8046  suplocexprlemrl  8048  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemub  8054  suplocexprlemlub  8055  recexgt0sr  8104  mulgt0sr  8109  archsr  8113  caucvgsrlemoffcau  8129  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  cnm  8163  axarch  8222  axcaucvglemcau  8229  axpre-suploclemres  8232  lelttr  8378  ltletr  8379  ltled  8409  cnegexlem1  8465  cnegexlem2  8466  renegcl  8551  negf1o  8673  gt0add  8865  apreap  8879  apirr  8897  apsym  8898  apcotr  8899  apadd1  8900  apneg  8903  mulext1  8904  mulap0r  8907  apti  8914  aprcl  8938  aptap  8942  recexap  8945  mulap0  8946  receuap  8963  mul0eqap  8964  lep1  9139  lem1  9141  letrp1  9142  recreclt  9194  lbinf  9242  suprubex  9245  nnrecgt0  9295  bndndx  9515  nn0ge2m1nn  9580  elnn0z  9610  peano2z  9633  zaddcl  9637  ztri3or0  9639  zltnle  9643  zdceq  9673  zdcle  9674  zdclt  9675  zdiv  9687  zeo  9704  fnn0ind  9715  btwnz  9718  uzm1  9906  uzp1  9909  indstr  9946  supinfneg  9948  infsupneg  9949  eluzdc  9963  nn01to3  9970  qapne  9992  xrltled  10154  xrlelttr  10161  xrltletr  10162  ge0nemnf  10179  fzdcel  10397  elfzouz2  10521  fzoss1  10532  fzospliti  10537  elincfzoext  10563  fzocatel  10569  fzostep1  10608  zsupcllemstep  10614  zsupcl  10616  infssuzledc  10619  qtri3or  10627  qltnle  10630  qdceq  10631  qdclt  10632  exbtwnzlemex  10636  rebtwn2zlemstep  10639  rebtwn2z  10641  qbtwnxr  10644  ioom  10647  ico0  10648  ioc0  10649  flqeqceilz  10707  modqadd1  10750  modqmul1  10766  frec2uzuzd  10791  frec2uzlt2d  10793  frec2uzf1od  10795  frecuzrdgrrn  10797  frec2uzrdg  10798  frecuzrdgrcl  10799  frecuzrdgsuc  10803  frecuzrdgrclt  10804  frecuzrdgdomlem  10806  uzsinds  10833  seqvalcd  10850  seqovcd  10856  seq3fveq2  10864  seqfveq2g  10866  seq3shft2  10870  seqshft2g  10871  monoord  10874  seq3split  10877  seqsplitg  10878  seq3caopr3  10880  iseqf1olemab  10891  iseqf1olemnanb  10892  iseqf1olemqk  10896  seqf1oglem1  10908  seqf1og  10910  seq3id3  10913  seq3id2  10915  seq3homo  10916  seqhomog  10919  expgt1  10966  m1expeven  10975  expnbnd  11053  expnlbnd2  11055  nn0ltexp2  11099  apexp1  11108  hashennn  11171  hashfibclem  11234  zfz1isolem1  11240  seq3coll  11242  pfxwrdsymbg  11410  wrdind  11442  wrd2ind  11443  cjap  11620  caucvgre  11695  cvg1nlemres  11699  resqrexlemgt0  11734  resqrexlemglsq  11736  resqrexlemga  11737  resqrtcl  11743  abslt  11802  abssubap0  11804  abssubne0  11805  caubnd2  11831  qdenre  11916  maxabslemlub  11921  maxabs  11923  maxleast  11927  fimaxre2  11941  xrmaxiflemlub  11962  xrmaxif  11965  xrmaxltsup  11972  xrmaxadd  11975  xrmineqinf  11983  climuni  12007  2clim  12015  climcn1  12022  climcn2  12023  subcn2  12025  mulcn2  12026  climsqz  12049  climsqz2  12050  climcau  12061  climcvg1nlem  12063  climcaucn  12065  serf0  12066  sumrbdclem  12092  summodclem2  12097  zsumdc  12099  divcnv  12212  absltap  12224  absgtap  12225  mertenslem2  12251  ntrivcvgap  12263  prodrbdclem  12286  prodmodclem2  12292  zproddc  12294  prodssdc  12304  fprodsplitdc  12311  fprodcl2lem  12320  efcllemp  12373  tanvalap  12423  sin01bnd  12472  cos01bnd  12473  sin01gt0  12477  absef  12485  eirrap  12493  dvds0  12521  dvdsmul1  12528  dvdsmultr1d  12547  dvdslelemd  12558  divconjdvds  12564  alzdvds  12569  3dvds  12579  sqoddm1div8z  12601  nno  12621  divalglemex  12637  bits0o  12665  dvdsbnd  12681  dvdslegcd  12689  zeqzmulgcd  12695  gcd0id  12704  gcdaddm  12709  gcd1  12712  gcdabs  12713  bezoutlemnewy  12721  bezoutlemstep  12722  bezoutlemmain  12723  bezoutlemex  12726  bezoutlemzz  12727  bezoutlemaz  12728  bezoutlembz  12729  bezoutlembi  12730  bezoutlemle  12733  bezoutlemsup  12734  mulgcd  12741  gcdzeq  12747  dvdsmulgcd  12750  sqgcd  12754  bezoutr1  12758  nninfctlemfo  12765  algcvga  12777  algfx  12778  eucalglt  12783  eucalg  12785  lcmneg  12800  lcmabs  12802  lcmgcdlem  12803  ncoprmgcdne1b  12815  mulgcddvds  12820  qredeq  12822  divgcdcoprm0  12827  cncongr1  12829  isprm2lem  12842  nprm  12849  dvdsnprmd  12851  prmdvdsfz  12865  isprm5lem  12867  coprm  12870  isprm6  12873  sqrt2irr  12888  pw2dvdslemn  12891  pw2dvdseulemle  12893  oddpwdclemdvds  12896  oddpwdclemndvds  12897  sqrt2irrap  12906  qnumdencl  12913  prmdiv  12961  modprmn0modprm0  12983  prm23lt5  12990  pythagtriplem4  12995  pythagtriplem19  13009  pythagtrip  13010  pclemub  13014  pcpre1  13019  pcpremul  13020  pceulem  13021  pcqcl  13033  pcidlem  13050  pcgcd1  13055  pc2dvds  13057  dvdsprmpweqle  13064  difsqpwdvds  13065  pcadd  13067  pcmpt  13070  expnprm  13080  pockthg  13084  infpnlem2  13087  prmunb  13089  1arith  13094  4sqlem10  13114  4sqlem11  13128  4sqlem12  13129  4sqlem13m  13130  4sqlem17  13134  4sqlem18  13135  ballotfilemfc0  13180  ballotfilemfcc  13181  ballotfilemfrceq  13220  ennnfonelemex  13253  ennnfonelemhom  13254  ennnfonelemrnh  13255  ennnfonelemnn0  13261  ennnfonelemim  13263  exmidunben  13265  ctinfomlemom  13266  ctinfom  13267  ctinf  13269  omctfn  13282  nninfdclemp1  13289  setscomd  13341  imasaddfnlemg  13582  mhmf1o  13729  grpinveu  13797  grpasscan1  13822  dfgrp3mlem  13857  grp1inv  13866  issubg4m  13950  ghmf1o  14032  srgisid  14233  ringadd2  14274  ringinvnzdiv  14297  unitgrp  14365  ringelnzr  14436  lringuplu  14445  subrguss  14486  subrgintm  14493  aprcotr  14539  islmodd  14571  lssclg  14642  lss0cl  14647  lssvneln0  14651  lss1d  14661  lmodindp1  14706  rnglidlmmgm  14774  znidomb  14936  znunit  14937  znrrg  14938  mplsubgfilemcl  14984  mplsubgfileminv  14985  tgcl  15059  neii1  15142  neii2  15144  neiss  15145  tpnei  15155  tgrest  15164  ssrest  15177  icnpimaex  15206  lmcvg  15212  cnpnei  15214  cnptopco  15217  lmff  15244  txcnp  15266  txcn  15270  hmeontr  15308  blssec  15433  mopni3  15479  blsscls2  15488  comet  15494  bdxmet  15496  bdmopn  15499  xmettxlem  15504  xmettx  15505  addcncntoplem  15556  mpomulcn  15561  mulc1cncf  15584  cncfco  15586  cncfmptc  15591  mulcncflem  15602  mulcncf  15603  dedekindeulemlu  15616  dedekindeulemeu  15617  suplociccreex  15619  suplociccex  15620  dedekindicclemlu  15625  dedekindicclemeu  15626  ivthinclemlopn  15631  ivthinclemlr  15632  ivthinclemuopn  15633  ivthinclemur  15634  ivthinclemloc  15636  ivthinc  15638  ivthreinc  15640  ivthdichlem  15646  limcimolemlt  15659  limcresi  15661  cnplimcim  15662  cnplimclemle  15663  cnplimclemr  15664  limccnpcntop  15670  limccoap  15673  dvcoapbr  15702  dvcj  15704  plyf  15732  plyaddlem1  15742  plymullem1  15743  plyco  15754  plycj  15756  plycn  15757  plyrecj  15758  dvply2g  15761  efltlemlt  15769  sin0pilem2  15777  tangtx  15833  logdivlti  15876  rplogbval  15940  logbgcd1irraplemexp  15963  logbgcd1irraplemap  15964  logbgcd1irrap  15965  perfect1  15996  perfectlem1  15997  perfectlem2  15998  lgsval4a  16025  lgsdir2lem3  16033  lgsne0  16041  gausslemma2dlem3  16066  gausslemma2dlem4  16067  gausslemma2dlem6  16070  gausslemma2dlem7  16071  gausslemma2d  16072  lgseisenlem1  16073  lgsquadlem2  16081  lgsquadlem3  16082  lgsquad2lem2  16085  lgsquad3  16087  2lgsoddprmlem2  16109  2sqlem8a  16125  2sqlem8  16126  2sqlem9  16127  lpvtx  16204  upgrex  16228  upgr1een  16249  edgupgren  16266  umgredg  16270  upgrpredgv  16271  upgredg2vtx  16273  upgredgpr  16274  uspgrf1oedg  16301  usgredg4  16340  uspgredgdomord  16354  usgr1vr  16373  wlkvtxiedg  16470  wlkvtxiedgg  16471  wlk1walkdom  16484  upgriswlkdc  16485  upgrwlkedg  16486  uspgr2wlkeq  16490  uspgr2wlkeqi  16492  umgrwlknloop  16493  eupth2lem2dc  16584  trlsegvdeglem1  16585  eupth2lem3lem4fi  16598  bj-exlimmpi  16682  uzdcinzz  16710  bj-charfundcALT  16719  bj-2inf  16848  bj-peano4  16865  bj-nn0suc  16874  pw1ndom3  16904  subctctexmid  16914  exmidcon  16920  nninfalllem1  16926  nninfsellemqall  16933  nninfomnilem  16936  nninffeq  16938  nnnninfex  16940  exmidsbthrlem  16942  sbthomlem  16945  refeq  16948  isomninnlem  16954  apdifflemr  16971  redcwlpo  16980  reap0  16983  nconstwlpolem  16990