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  1948  eqrdav  2231  necon1aidc  2463  necon1bidc  2464  necon4aidc  2480  reximddv  2645  reximssdv  2646  rexlimddv  2665  vtoclgft  2864  rspcedvd  2926  sseldd  3238  ssneldd  3240  tpid3g  3806  preq12b  3873  axpweq  4283  exmid1dc  4312  exmid1stab  4320  opth  4352  issod  4439  frirrg  4470  frind  4472  ralxfr2d  4584  rexxfr2d  4585  eldifpw  4597  onun2  4611  onuni  4615  elirr  4662  en2lp  4675  wetriext  4698  peano2  4716  relop  4904  elres  5073  sotri2  5159  iota4an  5332  iota5  5333  funeu  5376  funopg  5385  imadiflem  5434  funimaexglem  5438  ssimaex  5737  ffvelcdm  5809  dff3im  5821  dffo4  5824  funopsn  5859  f1eqcocnv  5963  f1oiso2  5999  riota5f  6029  riotass2  6031  acexmidlemcase  6044  elovimad  6093  ovmpodf  6184  ovmpodv2  6186  ovi3  6190  ov6g  6191  caoftrn  6298  op1steq  6372  fvdifsuppst  6443  suppssdc  6459  suppofss1dcl  6463  suppofss2dcl  6464  tfr0dm  6552  tfrlemibxssdm  6557  tfrlemi14d  6563  tfr1onlembxssdm  6573  tfr1onlemaccex  6578  tfr1onlemres  6579  tfrcllembxssdm  6586  tfrcllemaccex  6591  tfrcllemres  6592  rdgivallem  6611  nnsucelsuc  6723  nnsucsssuc  6724  dcdifsnid  6736  nnawordex  6761  ersym  6778  mapvalg  6891  pmvalg  6892  mapsnd  6922  mapsn  6924  fundmen  7046  1dom1el  7059  en2  7064  pw2f1odclem  7086  mapdom1g  7099  fidceq  7123  fin0or  7142  findcard2  7145  findcard2s  7146  fidcen  7155  prfidceq  7187  fiintim  7190  suplub2ti  7291  supsnti  7295  supisoex  7299  difinfsnlem  7389  difinfsn  7390  ctm  7399  ctssdclemn0  7400  ctssdccl  7401  ctssdc  7403  enumctlemm  7404  nninfninc  7413  nnnninfeq2  7419  enomnilem  7428  exmidomniim  7431  exmidomni  7432  fodjuomnilemdc  7434  fodjuomnilemres  7438  omnimkv  7446  mkvprop  7448  omniwomnimkv  7457  en2prde  7489  pr2cv1  7491  en2eleq  7497  acfun  7513  exmidontriimlem1  7527  exmidontriimlem4  7530  exmidontriim  7531  papsym  7560  papcotr  7561  ccfunen  7577  cc4f  7582  cc4n  7584  elni2  7628  mulclpi  7642  nlt1pig  7655  indpi  7656  recclnq  7706  ltexnqq  7722  halfnqq  7724  prarloclemarch  7732  prarloclemarch2  7733  prop  7789  prltlu  7801  prarloclem3step  7810  prarloclem5  7814  prarloclem  7815  prarloc  7817  prarloc2  7818  genpml  7831  genpmu  7832  genprndl  7835  genprndu  7836  genpdisj  7837  addnqprllem  7841  addnqprulem  7842  addlocprlemeq  7847  addlocprlemgt  7848  addlocprlem  7849  addlocpr  7850  nqprloc  7859  nqprl  7865  nqpru  7866  addnqprlemrl  7871  addnqprlemru  7872  appdivnq  7877  prmuloc  7880  prmuloc2  7881  mullocprlem  7884  mullocpr  7885  mulnqprlemrl  7887  mulnqprlemru  7888  ltprordil  7903  ltpopr  7909  ltsopr  7910  ltaddpr  7911  ltexprlemm  7914  ltexprlemopl  7915  ltexprlemlol  7916  ltexprlemopu  7917  ltexprlemupu  7918  ltexprlemloc  7921  ltexprlemfl  7923  ltexprlemrl  7924  ltexprlemfu  7925  ltexprlemru  7926  ltaprg  7933  recexprlemm  7938  recexprlem1ssl  7947  recexprlem1ssu  7948  aptiprleml  7953  aptiprlemu  7954  archpr  7957  cauappcvgprlemm  7959  cauappcvgprlemopl  7960  cauappcvgprlemlol  7961  cauappcvgprlemopu  7962  cauappcvgprlemupu  7963  cauappcvgprlemdisj  7965  cauappcvgprlemloc  7966  cauappcvgprlemladdfu  7968  cauappcvgprlemladdfl  7969  cauappcvgprlemladdru  7970  cauappcvgprlem1  7973  archrecpr  7978  caucvgprlemnkj  7980  caucvgprlemnbj  7981  caucvgprlemm  7982  caucvgprlemopl  7983  caucvgprlemlol  7984  caucvgprlemopu  7985  caucvgprlemupu  7986  caucvgprlemdisj  7988  caucvgprlemloc  7989  caucvgprlemladdfu  7991  caucvgprlem1  7993  caucvgprlemlim  7995  caucvgprprlemnbj  8007  caucvgprprlemml  8008  caucvgprprlemopl  8011  caucvgprprlemlol  8012  caucvgprprlemopu  8013  caucvgprprlemupu  8014  caucvgprprlemdisj  8016  caucvgprprlemloc  8017  caucvgprprlemexbt  8020  caucvgprprlemaddq  8022  caucvgprprlemlim  8025  suplocexprlemss  8029  suplocexprlemrl  8031  suplocexprlemmu  8032  suplocexprlemru  8033  suplocexprlemdisj  8034  suplocexprlemloc  8035  suplocexprlemub  8037  suplocexprlemlub  8038  recexgt0sr  8087  mulgt0sr  8092  archsr  8096  caucvgsrlemoffcau  8112  suplocsrlemb  8120  suplocsrlempr  8121  suplocsrlem  8122  cnm  8146  axarch  8205  axcaucvglemcau  8212  axpre-suploclemres  8215  lelttr  8361  ltletr  8362  ltled  8391  cnegexlem1  8447  cnegexlem2  8448  renegcl  8533  negf1o  8654  gt0add  8846  apreap  8860  apirr  8878  apsym  8879  apcotr  8880  apadd1  8881  apneg  8884  mulext1  8885  mulap0r  8888  apti  8895  aprcl  8919  aptap  8923  recexap  8926  mulap0  8927  receuap  8942  mul0eqap  8943  lep1  9118  lem1  9120  letrp1  9121  recreclt  9173  lbinf  9221  suprubex  9224  nnrecgt0  9274  bndndx  9494  nn0ge2m1nn  9559  elnn0z  9589  peano2z  9612  zaddcl  9616  ztri3or0  9618  zltnle  9622  zdceq  9652  zdcle  9653  zdclt  9654  zdiv  9665  zeo  9682  fnn0ind  9693  btwnz  9696  uzm1  9884  uzp1  9887  indstr  9924  supinfneg  9926  infsupneg  9927  eluzdc  9941  nn01to3  9948  qapne  9970  xrltled  10131  xrlelttr  10138  xrltletr  10139  ge0nemnf  10156  fzdcel  10373  elfzouz2  10495  fzoss1  10506  fzospliti  10511  elincfzoext  10537  fzocatel  10543  fzostep1  10582  zsupcllemstep  10588  zsupcl  10590  infssuzledc  10593  qtri3or  10599  qltnle  10602  qdceq  10603  qdclt  10604  exbtwnzlemex  10608  rebtwn2zlemstep  10611  rebtwn2z  10613  qbtwnxr  10616  ioom  10619  ico0  10620  ioc0  10621  flqeqceilz  10679  modqadd1  10722  modqmul1  10738  frec2uzuzd  10763  frec2uzlt2d  10765  frec2uzf1od  10767  frecuzrdgrrn  10769  frec2uzrdg  10770  frecuzrdgrcl  10771  frecuzrdgsuc  10775  frecuzrdgrclt  10776  frecuzrdgdomlem  10778  uzsinds  10805  seqvalcd  10822  seqovcd  10828  seq3fveq2  10836  seqfveq2g  10838  seq3shft2  10842  seqshft2g  10843  monoord  10846  seq3split  10849  seqsplitg  10850  seq3caopr3  10852  iseqf1olemab  10863  iseqf1olemnanb  10864  iseqf1olemqk  10868  seqf1oglem1  10880  seqf1og  10882  seq3id3  10885  seq3id2  10887  seq3homo  10888  seqhomog  10891  expgt1  10938  m1expeven  10947  expnbnd  11024  expnlbnd2  11026  nn0ltexp2  11070  apexp1  11079  hashennn  11141  hashfibclem  11202  zfz1isolem1  11208  seq3coll  11210  pfxwrdsymbg  11378  wrdind  11410  wrd2ind  11411  cjap  11587  caucvgre  11662  cvg1nlemres  11666  resqrexlemgt0  11701  resqrexlemglsq  11703  resqrexlemga  11704  resqrtcl  11710  abslt  11769  abssubap0  11771  abssubne0  11772  caubnd2  11798  qdenre  11883  maxabslemlub  11888  maxabs  11890  maxleast  11894  fimaxre2  11908  xrmaxiflemlub  11929  xrmaxif  11932  xrmaxltsup  11939  xrmaxadd  11942  xrmineqinf  11950  climuni  11974  2clim  11982  climcn1  11989  climcn2  11990  subcn2  11992  mulcn2  11993  climsqz  12016  climsqz2  12017  climcau  12028  climcvg1nlem  12030  climcaucn  12032  serf0  12033  sumrbdclem  12059  summodclem2  12064  zsumdc  12066  divcnv  12179  absltap  12191  absgtap  12192  mertenslem2  12218  ntrivcvgap  12230  prodrbdclem  12253  prodmodclem2  12259  zproddc  12261  prodssdc  12271  fprodsplitdc  12278  fprodcl2lem  12287  efcllemp  12340  tanvalap  12390  sin01bnd  12439  cos01bnd  12440  sin01gt0  12444  absef  12452  eirrap  12460  dvds0  12488  dvdsmul1  12495  dvdsmultr1d  12514  dvdslelemd  12525  divconjdvds  12531  alzdvds  12536  3dvds  12546  sqoddm1div8z  12568  nno  12588  divalglemex  12604  bits0o  12632  dvdsbnd  12648  dvdslegcd  12656  zeqzmulgcd  12662  gcd0id  12671  gcdaddm  12676  gcd1  12679  gcdabs  12680  bezoutlemnewy  12688  bezoutlemstep  12689  bezoutlemmain  12690  bezoutlemex  12693  bezoutlemzz  12694  bezoutlemaz  12695  bezoutlembz  12696  bezoutlembi  12697  bezoutlemle  12700  bezoutlemsup  12701  mulgcd  12708  gcdzeq  12714  dvdsmulgcd  12717  sqgcd  12721  bezoutr1  12725  nninfctlemfo  12732  algcvga  12744  algfx  12745  eucalglt  12750  eucalg  12752  lcmneg  12767  lcmabs  12769  lcmgcdlem  12770  ncoprmgcdne1b  12782  mulgcddvds  12787  qredeq  12789  divgcdcoprm0  12794  cncongr1  12796  isprm2lem  12809  nprm  12816  dvdsnprmd  12818  prmdvdsfz  12832  isprm5lem  12834  coprm  12837  isprm6  12840  sqrt2irr  12855  pw2dvdslemn  12858  pw2dvdseulemle  12860  oddpwdclemdvds  12863  oddpwdclemndvds  12864  sqrt2irrap  12873  qnumdencl  12880  prmdiv  12928  modprmn0modprm0  12950  prm23lt5  12957  pythagtriplem4  12962  pythagtriplem19  12976  pythagtrip  12977  pclemub  12981  pcpre1  12986  pcpremul  12987  pceulem  12988  pcqcl  13000  pcidlem  13017  pcgcd1  13022  pc2dvds  13024  dvdsprmpweqle  13031  difsqpwdvds  13032  pcadd  13034  pcmpt  13037  expnprm  13047  pockthg  13051  infpnlem2  13054  prmunb  13056  1arith  13061  4sqlem10  13081  4sqlem11  13095  4sqlem12  13096  4sqlem13m  13097  4sqlem17  13101  4sqlem18  13102  ennnfonelemex  13157  ennnfonelemhom  13158  ennnfonelemrnh  13159  ennnfonelemnn0  13165  ennnfonelemim  13167  exmidunben  13169  ctinfomlemom  13170  ctinfom  13171  ctinf  13173  omctfn  13186  nninfdclemp1  13193  setscomd  13245  imasaddfnlemg  13519  mhmf1o  13675  grpinveu  13743  grpasscan1  13768  dfgrp3mlem  13803  grp1inv  13812  issubg4m  13902  ghmf1o  13984  srgisid  14122  ringadd2  14163  ringinvnzdiv  14186  unitgrp  14253  ringelnzr  14324  lringuplu  14333  subrguss  14373  subrgintm  14380  aprcotr  14423  islmodd  14433  lssclg  14504  lss0cl  14509  lssvneln0  14513  lss1d  14523  lmodindp1  14568  rnglidlmmgm  14636  znidomb  14798  znunit  14799  znrrg  14800  mplsubgfilemcl  14846  mplsubgfileminv  14847  tgcl  14921  neii1  15004  neii2  15006  neiss  15007  tpnei  15017  tgrest  15026  ssrest  15039  icnpimaex  15068  lmcvg  15074  cnpnei  15076  cnptopco  15079  lmff  15106  txcnp  15128  txcn  15132  hmeontr  15170  blssec  15295  mopni3  15341  blsscls2  15350  comet  15356  bdxmet  15358  bdmopn  15361  xmettxlem  15366  xmettx  15367  addcncntoplem  15418  mpomulcn  15423  mulc1cncf  15446  cncfco  15448  cncfmptc  15453  mulcncflem  15464  mulcncf  15465  dedekindeulemlu  15478  dedekindeulemeu  15479  suplociccreex  15481  suplociccex  15482  dedekindicclemlu  15487  dedekindicclemeu  15488  ivthinclemlopn  15493  ivthinclemlr  15494  ivthinclemuopn  15495  ivthinclemur  15496  ivthinclemloc  15498  ivthinc  15500  ivthreinc  15502  ivthdichlem  15508  limcimolemlt  15521  limcresi  15523  cnplimcim  15524  cnplimclemle  15525  cnplimclemr  15526  limccnpcntop  15532  limccoap  15535  dvcoapbr  15564  dvcj  15566  plyf  15594  plyaddlem1  15604  plymullem1  15605  plyco  15616  plycj  15618  plycn  15619  plyrecj  15620  dvply2g  15623  efltlemlt  15631  sin0pilem2  15639  tangtx  15695  logdivlti  15738  rplogbval  15802  logbgcd1irraplemexp  15825  logbgcd1irraplemap  15826  logbgcd1irrap  15827  perfect1  15858  perfectlem1  15859  perfectlem2  15860  lgsval4a  15887  lgsdir2lem3  15895  lgsne0  15903  gausslemma2dlem3  15928  gausslemma2dlem4  15929  gausslemma2dlem6  15932  gausslemma2dlem7  15933  gausslemma2d  15934  lgseisenlem1  15935  lgsquadlem2  15943  lgsquadlem3  15944  lgsquad2lem2  15947  lgsquad3  15949  2lgsoddprmlem2  15971  2sqlem8a  15987  2sqlem8  15988  2sqlem9  15989  lpvtx  16066  upgrex  16090  upgr1een  16111  edgupgren  16128  umgredg  16132  upgrpredgv  16133  upgredg2vtx  16135  upgredgpr  16136  uspgrf1oedg  16163  usgredg4  16202  uspgredgdomord  16216  usgr1vr  16235  wlkvtxiedg  16332  wlkvtxiedgg  16333  wlk1walkdom  16346  upgriswlkdc  16347  upgrwlkedg  16348  uspgr2wlkeq  16352  uspgr2wlkeqi  16354  umgrwlknloop  16355  eupth2lem2dc  16446  trlsegvdeglem1  16447  eupth2lem3lem4fi  16460  bj-exlimmpi  16534  uzdcinzz  16562  bj-charfundcALT  16571  bj-2inf  16700  bj-peano4  16717  bj-nn0suc  16726  pw1ndom3  16756  subctctexmid  16766  exmidcon  16772  nninfalllem1  16778  nninfsellemqall  16785  nninfomnilem  16788  nninffeq  16790  nnnninfex  16792  exmidsbthrlem  16794  sbthomlem  16797  refeq  16800  isomninnlem  16806  apdifflemr  16823  redcwlpo  16832  reap0  16835  nconstwlpolem  16842