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  1920  exlimddv  1947  eqrdav  2230  necon1aidc  2454  necon1bidc  2455  necon4aidc  2471  reximddv  2636  reximssdv  2637  rexlimddv  2656  vtoclgft  2855  rspcedvd  2917  sseldd  3229  ssneldd  3231  tpid3g  3791  preq12b  3858  axpweq  4267  exmid1dc  4296  exmid1stab  4304  opth  4335  issod  4422  frirrg  4453  frind  4455  ralxfr2d  4567  rexxfr2d  4568  eldifpw  4580  onun2  4594  onuni  4598  elirr  4645  en2lp  4658  wetriext  4681  peano2  4699  relop  4886  elres  5055  sotri2  5141  iota4an  5314  iota5  5315  funeu  5358  funopg  5367  imadiflem  5416  funimaexglem  5420  ssimaex  5716  ffvelcdm  5788  dff3im  5800  dffo4  5803  funopsn  5838  f1eqcocnv  5942  f1oiso2  5978  riota5f  6008  riotass2  6010  acexmidlemcase  6023  elovimad  6072  ovmpodf  6163  ovmpodv2  6165  ovi3  6169  ov6g  6170  caoftrn  6277  op1steq  6351  fvdifsuppst  6422  suppssdc  6438  suppofss1dcl  6442  suppofss2dcl  6443  tfr0dm  6531  tfrlemibxssdm  6536  tfrlemi14d  6542  tfr1onlembxssdm  6552  tfr1onlemaccex  6557  tfr1onlemres  6558  tfrcllembxssdm  6565  tfrcllemaccex  6570  tfrcllemres  6571  rdgivallem  6590  nnsucelsuc  6702  nnsucsssuc  6703  dcdifsnid  6715  nnawordex  6740  ersym  6757  mapvalg  6870  pmvalg  6871  mapsn  6902  fundmen  7024  1dom1el  7036  en2  7041  pw2f1odclem  7063  mapdom1g  7076  fidceq  7099  fin0or  7118  findcard2  7121  findcard2s  7122  fidcen  7131  prfidceq  7163  fiintim  7166  suplub2ti  7243  supsnti  7247  supisoex  7251  difinfsnlem  7341  difinfsn  7342  ctm  7351  ctssdclemn0  7352  ctssdccl  7353  ctssdc  7355  enumctlemm  7356  nninfninc  7365  nnnninfeq2  7371  enomnilem  7380  exmidomniim  7383  exmidomni  7384  fodjuomnilemdc  7386  fodjuomnilemres  7390  omnimkv  7398  mkvprop  7400  omniwomnimkv  7409  en2prde  7441  pr2cv1  7443  en2eleq  7449  acfun  7465  exmidontriimlem1  7479  exmidontriimlem4  7482  exmidontriim  7483  ccfunen  7526  cc4f  7531  cc4n  7533  elni2  7577  mulclpi  7591  nlt1pig  7604  indpi  7605  recclnq  7655  ltexnqq  7671  halfnqq  7673  prarloclemarch  7681  prarloclemarch2  7682  prop  7738  prltlu  7750  prarloclem3step  7759  prarloclem5  7763  prarloclem  7764  prarloc  7766  prarloc2  7767  genpml  7780  genpmu  7781  genprndl  7784  genprndu  7785  genpdisj  7786  addnqprllem  7790  addnqprulem  7791  addlocprlemeq  7796  addlocprlemgt  7797  addlocprlem  7798  addlocpr  7799  nqprloc  7808  nqprl  7814  nqpru  7815  addnqprlemrl  7820  addnqprlemru  7821  appdivnq  7826  prmuloc  7829  prmuloc2  7830  mullocprlem  7833  mullocpr  7834  mulnqprlemrl  7836  mulnqprlemru  7837  ltprordil  7852  ltpopr  7858  ltsopr  7859  ltaddpr  7860  ltexprlemm  7863  ltexprlemopl  7864  ltexprlemlol  7865  ltexprlemopu  7866  ltexprlemupu  7867  ltexprlemloc  7870  ltexprlemfl  7872  ltexprlemrl  7873  ltexprlemfu  7874  ltexprlemru  7875  ltaprg  7882  recexprlemm  7887  recexprlem1ssl  7896  recexprlem1ssu  7897  aptiprleml  7902  aptiprlemu  7903  archpr  7906  cauappcvgprlemm  7908  cauappcvgprlemopl  7909  cauappcvgprlemlol  7910  cauappcvgprlemopu  7911  cauappcvgprlemupu  7912  cauappcvgprlemdisj  7914  cauappcvgprlemloc  7915  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  cauappcvgprlemladdru  7919  cauappcvgprlem1  7922  archrecpr  7927  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemm  7931  caucvgprlemopl  7932  caucvgprlemlol  7933  caucvgprlemopu  7934  caucvgprlemupu  7935  caucvgprlemdisj  7937  caucvgprlemloc  7938  caucvgprlemladdfu  7940  caucvgprlem1  7942  caucvgprlemlim  7944  caucvgprprlemnbj  7956  caucvgprprlemml  7957  caucvgprprlemopl  7960  caucvgprprlemlol  7961  caucvgprprlemopu  7962  caucvgprprlemupu  7963  caucvgprprlemdisj  7965  caucvgprprlemloc  7966  caucvgprprlemexbt  7969  caucvgprprlemaddq  7971  caucvgprprlemlim  7974  suplocexprlemss  7978  suplocexprlemrl  7980  suplocexprlemmu  7981  suplocexprlemru  7982  suplocexprlemdisj  7983  suplocexprlemloc  7984  suplocexprlemub  7986  suplocexprlemlub  7987  recexgt0sr  8036  mulgt0sr  8041  archsr  8045  caucvgsrlemoffcau  8061  suplocsrlemb  8069  suplocsrlempr  8070  suplocsrlem  8071  cnm  8095  axarch  8154  axcaucvglemcau  8161  axpre-suploclemres  8164  lelttr  8311  ltletr  8312  ltled  8341  cnegexlem1  8397  cnegexlem2  8398  renegcl  8483  negf1o  8604  gt0add  8796  apreap  8810  apirr  8828  apsym  8829  apcotr  8830  apadd1  8831  apneg  8834  mulext1  8835  mulap0r  8838  apti  8845  aprcl  8869  aptap  8873  recexap  8876  mulap0  8877  receuap  8892  mul0eqap  8893  lep1  9068  lem1  9070  letrp1  9071  recreclt  9123  lbinf  9171  suprubex  9174  nnrecgt0  9224  bndndx  9444  nn0ge2m1nn  9505  elnn0z  9535  peano2z  9558  zaddcl  9562  ztri3or0  9564  zltnle  9568  zdceq  9598  zdcle  9599  zdclt  9600  zdiv  9611  zeo  9628  fnn0ind  9639  btwnz  9642  uzm1  9830  uzp1  9833  indstr  9870  supinfneg  9872  infsupneg  9873  eluzdc  9887  nn01to3  9894  qapne  9916  xrltled  10077  xrlelttr  10084  xrltletr  10085  ge0nemnf  10102  fzdcel  10318  elfzouz2  10440  fzoss1  10451  fzospliti  10456  elincfzoext  10482  fzocatel  10488  fzostep1  10527  zsupcllemstep  10533  zsupcl  10535  infssuzledc  10538  qtri3or  10544  qltnle  10547  qdceq  10548  qdclt  10549  exbtwnzlemex  10553  rebtwn2zlemstep  10556  rebtwn2z  10558  qbtwnxr  10561  ioom  10564  ico0  10565  ioc0  10566  flqeqceilz  10624  modqadd1  10667  modqmul1  10683  frec2uzuzd  10708  frec2uzlt2d  10710  frec2uzf1od  10712  frecuzrdgrrn  10714  frec2uzrdg  10715  frecuzrdgrcl  10716  frecuzrdgsuc  10720  frecuzrdgrclt  10721  frecuzrdgdomlem  10723  uzsinds  10750  seqvalcd  10767  seqovcd  10773  seq3fveq2  10781  seqfveq2g  10783  seq3shft2  10787  seqshft2g  10788  monoord  10791  seq3split  10794  seqsplitg  10795  seq3caopr3  10797  iseqf1olemab  10808  iseqf1olemnanb  10809  iseqf1olemqk  10813  seqf1oglem1  10825  seqf1og  10827  seq3id3  10830  seq3id2  10832  seq3homo  10833  seqhomog  10836  expgt1  10883  m1expeven  10892  expnbnd  10969  expnlbnd2  10971  nn0ltexp2  11015  apexp1  11024  hashennn  11086  zfz1isolem1  11148  seq3coll  11150  pfxwrdsymbg  11318  wrdind  11350  wrd2ind  11351  cjap  11527  caucvgre  11602  cvg1nlemres  11606  resqrexlemgt0  11641  resqrexlemglsq  11643  resqrexlemga  11644  resqrtcl  11650  abslt  11709  abssubap0  11711  abssubne0  11712  caubnd2  11738  qdenre  11823  maxabslemlub  11828  maxabs  11830  maxleast  11834  fimaxre2  11848  xrmaxiflemlub  11869  xrmaxif  11872  xrmaxltsup  11879  xrmaxadd  11882  xrmineqinf  11890  climuni  11914  2clim  11922  climcn1  11929  climcn2  11930  subcn2  11932  mulcn2  11933  climsqz  11956  climsqz2  11957  climcau  11968  climcvg1nlem  11970  climcaucn  11972  serf0  11973  sumrbdclem  11999  summodclem2  12004  zsumdc  12006  divcnv  12119  absltap  12131  absgtap  12132  mertenslem2  12158  ntrivcvgap  12170  prodrbdclem  12193  prodmodclem2  12199  zproddc  12201  prodssdc  12211  fprodsplitdc  12218  fprodcl2lem  12227  efcllemp  12280  tanvalap  12330  sin01bnd  12379  cos01bnd  12380  sin01gt0  12384  absef  12392  eirrap  12400  dvds0  12428  dvdsmul1  12435  dvdsmultr1d  12454  dvdslelemd  12465  divconjdvds  12471  alzdvds  12476  3dvds  12486  sqoddm1div8z  12508  nno  12528  divalglemex  12544  bits0o  12572  dvdsbnd  12588  dvdslegcd  12596  zeqzmulgcd  12602  gcd0id  12611  gcdaddm  12616  gcd1  12619  gcdabs  12620  bezoutlemnewy  12628  bezoutlemstep  12629  bezoutlemmain  12630  bezoutlemex  12633  bezoutlemzz  12634  bezoutlemaz  12635  bezoutlembz  12636  bezoutlembi  12637  bezoutlemle  12640  bezoutlemsup  12641  mulgcd  12648  gcdzeq  12654  dvdsmulgcd  12657  sqgcd  12661  bezoutr1  12665  nninfctlemfo  12672  algcvga  12684  algfx  12685  eucalglt  12690  eucalg  12692  lcmneg  12707  lcmabs  12709  lcmgcdlem  12710  ncoprmgcdne1b  12722  mulgcddvds  12727  qredeq  12729  divgcdcoprm0  12734  cncongr1  12736  isprm2lem  12749  nprm  12756  dvdsnprmd  12758  prmdvdsfz  12772  isprm5lem  12774  coprm  12777  isprm6  12780  sqrt2irr  12795  pw2dvdslemn  12798  pw2dvdseulemle  12800  oddpwdclemdvds  12803  oddpwdclemndvds  12804  sqrt2irrap  12813  qnumdencl  12820  prmdiv  12868  modprmn0modprm0  12890  prm23lt5  12897  pythagtriplem4  12902  pythagtriplem19  12916  pythagtrip  12917  pclemub  12921  pcpre1  12926  pcpremul  12927  pceulem  12928  pcqcl  12940  pcidlem  12957  pcgcd1  12962  pc2dvds  12964  dvdsprmpweqle  12971  difsqpwdvds  12972  pcadd  12974  pcmpt  12977  expnprm  12987  pockthg  12991  infpnlem2  12994  prmunb  12996  1arith  13001  4sqlem10  13021  4sqlem11  13035  4sqlem12  13036  4sqlem13m  13037  4sqlem17  13041  4sqlem18  13042  ennnfonelemex  13096  ennnfonelemhom  13097  ennnfonelemrnh  13098  ennnfonelemnn0  13104  ennnfonelemim  13106  exmidunben  13108  ctinfomlemom  13109  ctinfom  13110  ctinf  13112  omctfn  13125  nninfdclemp1  13132  setscomd  13184  imasaddfnlemg  13458  mhmf1o  13614  grpinveu  13682  grpasscan1  13707  dfgrp3mlem  13742  grp1inv  13751  issubg4m  13841  ghmf1o  13923  srgisid  14061  ringadd2  14102  ringinvnzdiv  14125  unitgrp  14192  ringelnzr  14263  lringuplu  14272  subrguss  14312  subrgintm  14319  aprcotr  14361  islmodd  14369  lssclg  14440  lss0cl  14445  lssvneln0  14449  lss1d  14459  lmodindp1  14504  rnglidlmmgm  14572  znidomb  14734  znunit  14735  znrrg  14736  mplsubgfilemcl  14780  mplsubgfileminv  14781  tgcl  14855  neii1  14938  neii2  14940  neiss  14941  tpnei  14951  tgrest  14960  ssrest  14973  icnpimaex  15002  lmcvg  15008  cnpnei  15010  cnptopco  15013  lmff  15040  txcnp  15062  txcn  15066  hmeontr  15104  blssec  15229  mopni3  15275  blsscls2  15284  comet  15290  bdxmet  15292  bdmopn  15295  xmettxlem  15300  xmettx  15301  addcncntoplem  15352  mpomulcn  15357  mulc1cncf  15380  cncfco  15382  cncfmptc  15387  mulcncflem  15398  mulcncf  15399  dedekindeulemlu  15412  dedekindeulemeu  15413  suplociccreex  15415  suplociccex  15416  dedekindicclemlu  15421  dedekindicclemeu  15422  ivthinclemlopn  15427  ivthinclemlr  15428  ivthinclemuopn  15429  ivthinclemur  15430  ivthinclemloc  15432  ivthinc  15434  ivthreinc  15436  ivthdichlem  15442  limcimolemlt  15455  limcresi  15457  cnplimcim  15458  cnplimclemle  15459  cnplimclemr  15460  limccnpcntop  15466  limccoap  15469  dvcoapbr  15498  dvcj  15500  plyf  15528  plyaddlem1  15538  plymullem1  15539  plyco  15550  plycj  15552  plycn  15553  plyrecj  15554  dvply2g  15557  efltlemlt  15565  sin0pilem2  15573  tangtx  15629  logdivlti  15672  rplogbval  15736  logbgcd1irraplemexp  15759  logbgcd1irraplemap  15760  logbgcd1irrap  15761  perfect1  15792  perfectlem1  15793  perfectlem2  15794  lgsval4a  15821  lgsdir2lem3  15829  lgsne0  15837  gausslemma2dlem3  15862  gausslemma2dlem4  15863  gausslemma2dlem6  15866  gausslemma2dlem7  15867  gausslemma2d  15868  lgseisenlem1  15869  lgsquadlem2  15877  lgsquadlem3  15878  lgsquad2lem2  15881  lgsquad3  15883  2lgsoddprmlem2  15905  2sqlem8a  15921  2sqlem8  15922  2sqlem9  15923  lpvtx  16000  upgrex  16024  upgr1een  16045  edgupgren  16062  umgredg  16066  upgrpredgv  16067  upgredg2vtx  16069  upgredgpr  16070  uspgrf1oedg  16097  usgredg4  16136  uspgredgdomord  16150  usgr1vr  16169  wlkvtxiedg  16266  wlkvtxiedgg  16267  wlk1walkdom  16280  upgriswlkdc  16281  upgrwlkedg  16282  uspgr2wlkeq  16286  uspgr2wlkeqi  16288  umgrwlknloop  16289  eupth2lem2dc  16380  trlsegvdeglem1  16381  eupth2lem3lem4fi  16394  bj-exlimmpi  16468  uzdcinzz  16496  bj-charfundcALT  16505  bj-2inf  16634  bj-peano4  16651  bj-nn0suc  16660  pw1ndom3  16690  subctctexmid  16702  exmidcon  16708  nninfalllem1  16714  nninfsellemqall  16721  nninfomnilem  16724  nninffeq  16726  nnnninfex  16728  exmidsbthrlem  16730  sbthomlem  16733  refeq  16736  isomninnlem  16742  apdifflemr  16759  redcwlpo  16768  reap0  16771  nconstwlpolem  16778