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  623  mt2d  628  mpnanrd  697  mpjaod  723  stdcndcOLD  851  impidc  863  jadc  868  pm2.54dc  896  oplem1  981  mp3and  1374  xor3dc  1429  exlimdd  1918  exlimddv  1945  eqrdav  2228  necon1aidc  2451  necon1bidc  2452  necon4aidc  2468  reximddv  2633  reximssdv  2634  rexlimddv  2653  vtoclgft  2852  rspcedvd  2914  sseldd  3226  ssneldd  3228  tpid3g  3785  preq12b  3851  axpweq  4259  exmid1dc  4288  exmid1stab  4296  opth  4327  issod  4414  frirrg  4445  frind  4447  ralxfr2d  4559  rexxfr2d  4560  eldifpw  4572  onun2  4586  onuni  4590  elirr  4637  en2lp  4650  wetriext  4673  peano2  4691  relop  4878  elres  5047  sotri2  5132  iota4an  5305  iota5  5306  funeu  5349  funopg  5358  imadiflem  5406  funimaexglem  5410  ssimaex  5703  ffvelcdm  5776  dff3im  5788  dffo4  5791  funopsn  5825  f1eqcocnv  5927  f1oiso2  5963  riota5f  5993  riotass2  5995  acexmidlemcase  6008  elovimad  6057  ovmpodf  6148  ovmpodv2  6150  ovi3  6154  ov6g  6155  caoftrn  6263  op1steq  6337  tfr0dm  6483  tfrlemibxssdm  6488  tfrlemi14d  6494  tfr1onlembxssdm  6504  tfr1onlemaccex  6509  tfr1onlemres  6510  tfrcllembxssdm  6517  tfrcllemaccex  6522  tfrcllemres  6523  rdgivallem  6542  nnsucelsuc  6654  nnsucsssuc  6655  dcdifsnid  6667  nnawordex  6692  ersym  6709  mapvalg  6822  pmvalg  6823  mapsn  6854  fundmen  6976  1dom1el  6988  en2  6993  pw2f1odclem  7015  mapdom1g  7028  fidceq  7051  fin0or  7070  findcard2  7073  findcard2s  7074  fidcen  7083  prfidceq  7115  fiintim  7118  suplub2ti  7194  supsnti  7198  supisoex  7202  difinfsnlem  7292  difinfsn  7293  ctm  7302  ctssdclemn0  7303  ctssdccl  7304  ctssdc  7306  enumctlemm  7307  nninfninc  7316  nnnninfeq2  7322  enomnilem  7331  exmidomniim  7334  exmidomni  7335  fodjuomnilemdc  7337  fodjuomnilemres  7341  omnimkv  7349  mkvprop  7351  omniwomnimkv  7360  en2prde  7392  pr2cv1  7394  en2eleq  7399  acfun  7415  exmidontriimlem1  7429  exmidontriimlem4  7432  exmidontriim  7433  ccfunen  7476  cc4f  7481  cc4n  7483  elni2  7527  mulclpi  7541  nlt1pig  7554  indpi  7555  recclnq  7605  ltexnqq  7621  halfnqq  7623  prarloclemarch  7631  prarloclemarch2  7632  prop  7688  prltlu  7700  prarloclem3step  7709  prarloclem5  7713  prarloclem  7714  prarloc  7716  prarloc2  7717  genpml  7730  genpmu  7731  genprndl  7734  genprndu  7735  genpdisj  7736  addnqprllem  7740  addnqprulem  7741  addlocprlemeq  7746  addlocprlemgt  7747  addlocprlem  7748  addlocpr  7749  nqprloc  7758  nqprl  7764  nqpru  7765  addnqprlemrl  7770  addnqprlemru  7771  appdivnq  7776  prmuloc  7779  prmuloc2  7780  mullocprlem  7783  mullocpr  7784  mulnqprlemrl  7786  mulnqprlemru  7787  ltprordil  7802  ltpopr  7808  ltsopr  7809  ltaddpr  7810  ltexprlemm  7813  ltexprlemopl  7814  ltexprlemlol  7815  ltexprlemopu  7816  ltexprlemupu  7817  ltexprlemloc  7820  ltexprlemfl  7822  ltexprlemrl  7823  ltexprlemfu  7824  ltexprlemru  7825  ltaprg  7832  recexprlemm  7837  recexprlem1ssl  7846  recexprlem1ssu  7847  aptiprleml  7852  aptiprlemu  7853  archpr  7856  cauappcvgprlemm  7858  cauappcvgprlemopl  7859  cauappcvgprlemlol  7860  cauappcvgprlemopu  7861  cauappcvgprlemupu  7862  cauappcvgprlemdisj  7864  cauappcvgprlemloc  7865  cauappcvgprlemladdfu  7867  cauappcvgprlemladdfl  7868  cauappcvgprlemladdru  7869  cauappcvgprlem1  7872  archrecpr  7877  caucvgprlemnkj  7879  caucvgprlemnbj  7880  caucvgprlemm  7881  caucvgprlemopl  7882  caucvgprlemlol  7883  caucvgprlemopu  7884  caucvgprlemupu  7885  caucvgprlemdisj  7887  caucvgprlemloc  7888  caucvgprlemladdfu  7890  caucvgprlem1  7892  caucvgprlemlim  7894  caucvgprprlemnbj  7906  caucvgprprlemml  7907  caucvgprprlemopl  7910  caucvgprprlemlol  7911  caucvgprprlemopu  7912  caucvgprprlemupu  7913  caucvgprprlemdisj  7915  caucvgprprlemloc  7916  caucvgprprlemexbt  7919  caucvgprprlemaddq  7921  caucvgprprlemlim  7924  suplocexprlemss  7928  suplocexprlemrl  7930  suplocexprlemmu  7931  suplocexprlemru  7932  suplocexprlemdisj  7933  suplocexprlemloc  7934  suplocexprlemub  7936  suplocexprlemlub  7937  recexgt0sr  7986  mulgt0sr  7991  archsr  7995  caucvgsrlemoffcau  8011  suplocsrlemb  8019  suplocsrlempr  8020  suplocsrlem  8021  cnm  8045  axarch  8104  axcaucvglemcau  8111  axpre-suploclemres  8114  lelttr  8261  ltletr  8262  ltled  8291  cnegexlem1  8347  cnegexlem2  8348  renegcl  8433  negf1o  8554  gt0add  8746  apreap  8760  apirr  8778  apsym  8779  apcotr  8780  apadd1  8781  apneg  8784  mulext1  8785  mulap0r  8788  apti  8795  aprcl  8819  aptap  8823  recexap  8826  mulap0  8827  receuap  8842  mul0eqap  8843  lep1  9018  lem1  9020  letrp1  9021  recreclt  9073  lbinf  9121  suprubex  9124  nnrecgt0  9174  bndndx  9394  nn0ge2m1nn  9455  elnn0z  9485  peano2z  9508  zaddcl  9512  ztri3or0  9514  zltnle  9518  zdceq  9548  zdcle  9549  zdclt  9550  zdiv  9561  zeo  9578  fnn0ind  9589  btwnz  9592  uzm1  9780  uzp1  9783  indstr  9820  supinfneg  9822  infsupneg  9823  eluzdc  9837  nn01to3  9844  qapne  9866  xrltled  10027  xrlelttr  10034  xrltletr  10035  ge0nemnf  10052  fzdcel  10268  elfzouz2  10390  fzoss1  10401  fzospliti  10406  elincfzoext  10431  fzocatel  10437  fzostep1  10476  zsupcllemstep  10482  zsupcl  10484  infssuzledc  10487  qtri3or  10493  qltnle  10496  qdceq  10497  qdclt  10498  exbtwnzlemex  10502  rebtwn2zlemstep  10505  rebtwn2z  10507  qbtwnxr  10510  ioom  10513  ico0  10514  ioc0  10515  flqeqceilz  10573  modqadd1  10616  modqmul1  10632  frec2uzuzd  10657  frec2uzlt2d  10659  frec2uzf1od  10661  frecuzrdgrrn  10663  frec2uzrdg  10664  frecuzrdgrcl  10665  frecuzrdgsuc  10669  frecuzrdgrclt  10670  frecuzrdgdomlem  10672  uzsinds  10699  seqvalcd  10716  seqovcd  10722  seq3fveq2  10730  seqfveq2g  10732  seq3shft2  10736  seqshft2g  10737  monoord  10740  seq3split  10743  seqsplitg  10744  seq3caopr3  10746  iseqf1olemab  10757  iseqf1olemnanb  10758  iseqf1olemqk  10762  seqf1oglem1  10774  seqf1og  10776  seq3id3  10779  seq3id2  10781  seq3homo  10782  seqhomog  10785  expgt1  10832  m1expeven  10841  expnbnd  10918  expnlbnd2  10920  nn0ltexp2  10964  apexp1  10973  hashennn  11035  zfz1isolem1  11097  seq3coll  11099  pfxwrdsymbg  11264  wrdind  11296  wrd2ind  11297  cjap  11460  caucvgre  11535  cvg1nlemres  11539  resqrexlemgt0  11574  resqrexlemglsq  11576  resqrexlemga  11577  resqrtcl  11583  abslt  11642  abssubap0  11644  abssubne0  11645  caubnd2  11671  qdenre  11756  maxabslemlub  11761  maxabs  11763  maxleast  11767  fimaxre2  11781  xrmaxiflemlub  11802  xrmaxif  11805  xrmaxltsup  11812  xrmaxadd  11815  xrmineqinf  11823  climuni  11847  2clim  11855  climcn1  11862  climcn2  11863  subcn2  11865  mulcn2  11866  climsqz  11889  climsqz2  11890  climcau  11901  climcvg1nlem  11903  climcaucn  11905  serf0  11906  sumrbdclem  11931  summodclem2  11936  zsumdc  11938  divcnv  12051  absltap  12063  absgtap  12064  mertenslem2  12090  ntrivcvgap  12102  prodrbdclem  12125  prodmodclem2  12131  zproddc  12133  prodssdc  12143  fprodsplitdc  12150  fprodcl2lem  12159  efcllemp  12212  tanvalap  12262  sin01bnd  12311  cos01bnd  12312  sin01gt0  12316  absef  12324  eirrap  12332  dvds0  12360  dvdsmul1  12367  dvdsmultr1d  12386  dvdslelemd  12397  divconjdvds  12403  alzdvds  12408  3dvds  12418  sqoddm1div8z  12440  nno  12460  divalglemex  12476  bits0o  12504  dvdsbnd  12520  dvdslegcd  12528  zeqzmulgcd  12534  gcd0id  12543  gcdaddm  12548  gcd1  12551  gcdabs  12552  bezoutlemnewy  12560  bezoutlemstep  12561  bezoutlemmain  12562  bezoutlemex  12565  bezoutlemzz  12566  bezoutlemaz  12567  bezoutlembz  12568  bezoutlembi  12569  bezoutlemle  12572  bezoutlemsup  12573  mulgcd  12580  gcdzeq  12586  dvdsmulgcd  12589  sqgcd  12593  bezoutr1  12597  nninfctlemfo  12604  algcvga  12616  algfx  12617  eucalglt  12622  eucalg  12624  lcmneg  12639  lcmabs  12641  lcmgcdlem  12642  ncoprmgcdne1b  12654  mulgcddvds  12659  qredeq  12661  divgcdcoprm0  12666  cncongr1  12668  isprm2lem  12681  nprm  12688  dvdsnprmd  12690  prmdvdsfz  12704  isprm5lem  12706  coprm  12709  isprm6  12712  sqrt2irr  12727  pw2dvdslemn  12730  pw2dvdseulemle  12732  oddpwdclemdvds  12735  oddpwdclemndvds  12736  sqrt2irrap  12745  qnumdencl  12752  prmdiv  12800  modprmn0modprm0  12822  prm23lt5  12829  pythagtriplem4  12834  pythagtriplem19  12848  pythagtrip  12849  pclemub  12853  pcpre1  12858  pcpremul  12859  pceulem  12860  pcqcl  12872  pcidlem  12889  pcgcd1  12894  pc2dvds  12896  dvdsprmpweqle  12903  difsqpwdvds  12904  pcadd  12906  pcmpt  12909  expnprm  12919  pockthg  12923  infpnlem2  12926  prmunb  12928  1arith  12933  4sqlem10  12953  4sqlem11  12967  4sqlem12  12968  4sqlem13m  12969  4sqlem17  12973  4sqlem18  12974  ennnfonelemex  13028  ennnfonelemhom  13029  ennnfonelemrnh  13030  ennnfonelemnn0  13036  ennnfonelemim  13038  exmidunben  13040  ctinfomlemom  13041  ctinfom  13042  ctinf  13044  omctfn  13057  nninfdclemp1  13064  setscomd  13116  imasaddfnlemg  13390  mhmf1o  13546  grpinveu  13614  grpasscan1  13639  dfgrp3mlem  13674  grp1inv  13683  issubg4m  13773  ghmf1o  13855  srgisid  13992  ringadd2  14033  ringinvnzdiv  14056  unitgrp  14123  ringelnzr  14194  lringuplu  14203  subrguss  14243  subrgintm  14250  aprcotr  14292  islmodd  14300  lssclg  14371  lss0cl  14376  lssvneln0  14380  lss1d  14390  lmodindp1  14435  rnglidlmmgm  14503  znidomb  14665  znunit  14666  znrrg  14667  mplsubgfilemcl  14706  mplsubgfileminv  14707  tgcl  14781  neii1  14864  neii2  14866  neiss  14867  tpnei  14877  tgrest  14886  ssrest  14899  icnpimaex  14928  lmcvg  14934  cnpnei  14936  cnptopco  14939  lmff  14966  txcnp  14988  txcn  14992  hmeontr  15030  blssec  15155  mopni3  15201  blsscls2  15210  comet  15216  bdxmet  15218  bdmopn  15221  xmettxlem  15226  xmettx  15227  addcncntoplem  15278  mpomulcn  15283  mulc1cncf  15306  cncfco  15308  cncfmptc  15313  mulcncflem  15324  mulcncf  15325  dedekindeulemlu  15338  dedekindeulemeu  15339  suplociccreex  15341  suplociccex  15342  dedekindicclemlu  15347  dedekindicclemeu  15348  ivthinclemlopn  15353  ivthinclemlr  15354  ivthinclemuopn  15355  ivthinclemur  15356  ivthinclemloc  15358  ivthinc  15360  ivthreinc  15362  ivthdichlem  15368  limcimolemlt  15381  limcresi  15383  cnplimcim  15384  cnplimclemle  15385  cnplimclemr  15386  limccnpcntop  15392  limccoap  15395  dvcoapbr  15424  dvcj  15426  plyf  15454  plyaddlem1  15464  plymullem1  15465  plyco  15476  plycj  15478  plycn  15479  plyrecj  15480  dvply2g  15483  efltlemlt  15491  sin0pilem2  15499  tangtx  15555  logdivlti  15598  rplogbval  15662  logbgcd1irraplemexp  15685  logbgcd1irraplemap  15686  logbgcd1irrap  15687  perfect1  15715  perfectlem1  15716  perfectlem2  15717  lgsval4a  15744  lgsdir2lem3  15752  lgsne0  15760  gausslemma2dlem3  15785  gausslemma2dlem4  15786  gausslemma2dlem6  15789  gausslemma2dlem7  15790  gausslemma2d  15791  lgseisenlem1  15792  lgsquadlem2  15800  lgsquadlem3  15801  lgsquad2lem2  15804  lgsquad3  15806  2lgsoddprmlem2  15828  2sqlem8a  15844  2sqlem8  15845  2sqlem9  15846  lpvtx  15923  upgrex  15947  upgr1een  15968  edgupgren  15985  umgredg  15989  upgrpredgv  15990  upgredg2vtx  15992  upgredgpr  15993  uspgrf1oedg  16020  usgredg4  16059  uspgredgdomord  16073  usgr1vr  16092  wlkvtxiedg  16156  wlkvtxiedgg  16157  wlk1walkdom  16170  upgriswlkdc  16171  upgrwlkedg  16172  uspgr2wlkeq  16176  uspgr2wlkeqi  16178  umgrwlknloop  16179  bj-exlimmpi  16316  uzdcinzz  16344  bj-charfundcALT  16354  bj-2inf  16483  bj-peano4  16500  bj-nn0suc  16509  pw1ndom3  16539  subctctexmid  16551  nninfalllem1  16560  nninfsellemqall  16567  nninfomnilem  16570  nninffeq  16572  nnnninfex  16574  exmidsbthrlem  16576  sbthomlem  16579  refeq  16582  isomninnlem  16584  apdifflemr  16601  redcwlpo  16609  reap0  16612  nconstwlpolem  16619