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  146  mpbird  166  jcai  309  mp2and  430  pm2.21dd  610  mt2d  615  mpjaod  708  stdcndcOLD  832  impidc  844  jadc  849  pm2.54dc  877  pm4.55dc  923  oplem1  960  mp3and  1319  xor3dc  1366  exlimdd  1845  exlimddv  1871  eqrdav  2139  necon1aidc  2360  necon1bidc  2361  necon4aidc  2377  reximddv  2538  reximssdv  2539  rexlimddv  2557  vtoclgft  2739  rspcedvd  2799  sseldd  3103  ssneldd  3105  tpid3g  3646  preq12b  3705  axpweq  4103  exmid1dc  4131  opth  4167  issod  4249  frirrg  4280  frind  4282  ralxfr2d  4393  rexxfr2d  4394  eldifpw  4406  onun2  4414  onuni  4418  elirr  4464  en2lp  4477  wetriext  4499  peano2  4517  relop  4697  elres  4863  sotri2  4944  iota4an  5115  iota5  5116  funeu  5156  funopg  5165  imadiflem  5210  funimaexglem  5214  ssimaex  5490  ffvelrn  5561  dff3im  5573  dffo4  5576  f1eqcocnv  5700  f1oiso2  5736  riota5f  5762  riotass2  5764  acexmidlemcase  5777  ovmpodf  5910  ovmpodv2  5912  ovi3  5915  ov6g  5916  caoftrn  6015  op1steq  6085  tfr0dm  6227  tfrlemibxssdm  6232  tfrlemi14d  6238  tfr1onlembxssdm  6248  tfr1onlemaccex  6253  tfr1onlemres  6254  tfrcllembxssdm  6261  tfrcllemaccex  6266  tfrcllemres  6267  rdgivallem  6286  nnsucelsuc  6395  nnsucsssuc  6396  dcdifsnid  6408  nnawordex  6432  ersym  6449  mapvalg  6560  pmvalg  6561  mapsn  6592  fundmen  6708  mapdom1g  6749  fidceq  6771  fin0or  6788  findcard2  6791  findcard2s  6792  fiintim  6825  suplub2ti  6896  supsnti  6900  supisoex  6904  difinfsnlem  6992  difinfsn  6993  ctm  7002  ctssdclemn0  7003  ctssdccl  7004  ctssdc  7006  enumctlemm  7007  enomnilem  7018  exmidomniim  7021  exmidomni  7022  fodjuomnilemdc  7024  fodjuomnilemres  7028  omnimkv  7038  mkvprop  7040  omniwomnimkv  7049  en2eleq  7068  acfun  7080  ccfunen  7096  cc4f  7101  cc4n  7103  elni2  7146  mulclpi  7160  nlt1pig  7173  indpi  7174  recclnq  7224  ltexnqq  7240  halfnqq  7242  prarloclemarch  7250  prarloclemarch2  7251  prop  7307  prltlu  7319  prarloclem3step  7328  prarloclem5  7332  prarloclem  7333  prarloc  7335  prarloc2  7336  genpml  7349  genpmu  7350  genprndl  7353  genprndu  7354  genpdisj  7355  addnqprllem  7359  addnqprulem  7360  addlocprlemeq  7365  addlocprlemgt  7366  addlocprlem  7367  addlocpr  7368  nqprloc  7377  nqprl  7383  nqpru  7384  addnqprlemrl  7389  addnqprlemru  7390  appdivnq  7395  prmuloc  7398  prmuloc2  7399  mullocprlem  7402  mullocpr  7403  mulnqprlemrl  7405  mulnqprlemru  7406  ltprordil  7421  ltpopr  7427  ltsopr  7428  ltaddpr  7429  ltexprlemm  7432  ltexprlemopl  7433  ltexprlemlol  7434  ltexprlemopu  7435  ltexprlemupu  7436  ltexprlemloc  7439  ltexprlemfl  7441  ltexprlemrl  7442  ltexprlemfu  7443  ltexprlemru  7444  ltaprg  7451  recexprlemm  7456  recexprlem1ssl  7465  recexprlem1ssu  7466  aptiprleml  7471  aptiprlemu  7472  archpr  7475  cauappcvgprlemm  7477  cauappcvgprlemopl  7478  cauappcvgprlemlol  7479  cauappcvgprlemopu  7480  cauappcvgprlemupu  7481  cauappcvgprlemdisj  7483  cauappcvgprlemloc  7484  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  cauappcvgprlemladdru  7488  cauappcvgprlem1  7491  archrecpr  7496  caucvgprlemnkj  7498  caucvgprlemnbj  7499  caucvgprlemm  7500  caucvgprlemopl  7501  caucvgprlemlol  7502  caucvgprlemopu  7503  caucvgprlemupu  7504  caucvgprlemdisj  7506  caucvgprlemloc  7507  caucvgprlemladdfu  7509  caucvgprlem1  7511  caucvgprlemlim  7513  caucvgprprlemnbj  7525  caucvgprprlemml  7526  caucvgprprlemopl  7529  caucvgprprlemlol  7530  caucvgprprlemopu  7531  caucvgprprlemupu  7532  caucvgprprlemdisj  7534  caucvgprprlemloc  7535  caucvgprprlemexbt  7538  caucvgprprlemaddq  7540  caucvgprprlemlim  7543  suplocexprlemss  7547  suplocexprlemrl  7549  suplocexprlemmu  7550  suplocexprlemru  7551  suplocexprlemdisj  7552  suplocexprlemloc  7553  suplocexprlemub  7555  suplocexprlemlub  7556  recexgt0sr  7605  mulgt0sr  7610  archsr  7614  caucvgsrlemoffcau  7630  suplocsrlemb  7638  suplocsrlempr  7639  suplocsrlem  7640  cnm  7664  axarch  7723  axcaucvglemcau  7730  axpre-suploclemres  7733  lelttr  7876  ltletr  7877  ltled  7905  cnegexlem1  7961  cnegexlem2  7962  renegcl  8047  negf1o  8168  gt0add  8359  apreap  8373  apirr  8391  apsym  8392  apcotr  8393  apadd1  8394  apneg  8397  mulext1  8398  mulap0r  8401  apti  8408  aprcl  8432  recexap  8438  mulap0  8439  receuap  8454  mul0eqap  8455  lep1  8627  lem1  8629  letrp1  8630  recreclt  8682  lbinf  8730  suprubex  8733  nnrecgt0  8782  bndndx  9000  nn0ge2m1nn  9061  elnn0z  9091  peano2z  9114  zaddcl  9118  ztri3or0  9120  zltnle  9124  zdceq  9150  zdcle  9151  zdclt  9152  zdiv  9163  zeo  9180  fnn0ind  9191  btwnz  9194  uzm1  9380  uzp1  9383  indstr  9415  supinfneg  9417  infsupneg  9418  eluzdc  9431  nn01to3  9436  qapne  9458  xrltled  9615  xrlelttr  9619  xrltletr  9620  ge0nemnf  9637  fzdcel  9851  elfzouz2  9969  fzoss1  9979  fzospliti  9984  fzocatel  10007  fzostep1  10045  qtri3or  10051  qltnle  10054  qdceq  10055  exbtwnzlemex  10058  rebtwn2zlemstep  10061  rebtwn2z  10063  qbtwnxr  10066  ioom  10069  ico0  10070  ioc0  10071  flqeqceilz  10122  modqadd1  10165  modqmul1  10181  frec2uzuzd  10206  frec2uzlt2d  10208  frec2uzf1od  10210  frecuzrdgrrn  10212  frec2uzrdg  10213  frecuzrdgrcl  10214  frecuzrdgsuc  10218  frecuzrdgrclt  10219  frecuzrdgdomlem  10221  uzsinds  10246  seqvalcd  10263  seqovcd  10267  seq3fveq2  10273  seq3shft2  10277  monoord  10280  seq3split  10283  seq3caopr3  10285  iseqf1olemab  10293  iseqf1olemnanb  10294  iseqf1olemqk  10298  seq3id3  10311  seq3id2  10313  seq3homo  10314  expgt1  10362  m1expeven  10371  expnbnd  10446  expnlbnd2  10448  apexp1  10496  hashennn  10558  zfz1isolem1  10615  seq3coll  10617  cjap  10710  caucvgre  10785  cvg1nlemres  10789  resqrexlemgt0  10824  resqrexlemglsq  10826  resqrexlemga  10827  resqrtcl  10833  abslt  10892  abssubap0  10894  abssubne0  10895  caubnd2  10921  qdenre  11006  maxabslemlub  11011  maxabs  11013  maxleast  11017  fimaxre2  11030  xrmaxiflemlub  11049  xrmaxif  11052  xrmaxltsup  11059  xrmaxadd  11062  xrmineqinf  11070  climuni  11094  2clim  11102  climcn1  11109  climcn2  11110  subcn2  11112  mulcn2  11113  climsqz  11136  climsqz2  11137  climcau  11148  climcvg1nlem  11150  climcaucn  11152  serf0  11153  sumrbdclem  11178  summodclem2  11183  zsumdc  11185  divcnv  11298  absltap  11310  absgtap  11311  mertenslem2  11337  ntrivcvgap  11349  prodrbdclem  11372  prodmodclem2  11378  zproddc  11380  efcllemp  11401  tanvalap  11451  sin01bnd  11500  cos01bnd  11501  sin01gt0  11504  absef  11512  eirrap  11520  dvds0  11544  dvdsmul1  11551  dvdsmultr1d  11568  dvdslelemd  11577  divconjdvds  11583  alzdvds  11588  sqoddm1div8z  11619  nno  11639  divalglemex  11655  zsupcllemstep  11674  zsupcl  11676  infssuzledc  11679  dvdsbnd  11681  dvdslegcd  11689  zeqzmulgcd  11695  gcd0id  11703  gcdaddm  11708  gcd1  11711  gcdabs  11712  bezoutlemnewy  11720  bezoutlemstep  11721  bezoutlemmain  11722  bezoutlemex  11725  bezoutlemzz  11726  bezoutlemaz  11727  bezoutlembz  11728  bezoutlembi  11729  bezoutlemle  11732  bezoutlemsup  11733  mulgcd  11740  gcdzeq  11746  dvdsmulgcd  11749  sqgcd  11753  bezoutr1  11757  algcvga  11768  algfx  11769  eucalglt  11774  eucalg  11776  lcmneg  11791  lcmabs  11793  lcmgcdlem  11794  ncoprmgcdne1b  11806  mulgcddvds  11811  qredeq  11813  divgcdcoprm0  11818  cncongr1  11820  isprm2lem  11833  nprm  11840  dvdsnprmd  11842  prmdvdsfz  11855  coprm  11858  isprm6  11861  sqrt2irr  11876  pw2dvdslemn  11879  pw2dvdseulemle  11881  oddpwdclemdvds  11884  oddpwdclemndvds  11885  sqrt2irrap  11894  qnumdencl  11901  ennnfonelemex  11963  ennnfonelemhom  11964  ennnfonelemrnh  11965  ennnfonelemnn0  11971  ennnfonelemim  11973  exmidunben  11975  ctinfomlemom  11976  ctinfom  11977  ctinf  11979  omctfn  11992  tgcl  12272  neii1  12355  neii2  12357  neiss  12358  tpnei  12368  tgrest  12377  ssrest  12390  icnpimaex  12419  lmcvg  12425  cnpnei  12427  cnptopco  12430  lmff  12457  txcnp  12479  txcn  12483  hmeontr  12521  blssec  12646  mopni3  12692  blsscls2  12701  comet  12707  bdxmet  12709  bdmopn  12712  xmettxlem  12717  xmettx  12718  addcncntoplem  12759  mulc1cncf  12784  cncfco  12786  cncfmptc  12790  mulcncflem  12798  mulcncf  12799  dedekindeulemlu  12807  dedekindeulemeu  12808  suplociccreex  12810  suplociccex  12811  dedekindicclemlu  12816  dedekindicclemeu  12817  ivthinclemlopn  12822  ivthinclemlr  12823  ivthinclemuopn  12824  ivthinclemur  12825  ivthinclemloc  12827  ivthinc  12829  limcimolemlt  12841  limcresi  12843  cnplimcim  12844  cnplimclemle  12845  cnplimclemr  12846  limccnpcntop  12852  limccoap  12855  dvcoapbr  12879  dvcj  12881  efltlemlt  12903  sin0pilem2  12911  tangtx  12967  logdivlti  13010  rplogbval  13070  logbgcd1irraplemexp  13093  logbgcd1irraplemap  13094  logbgcd1irrap  13095  bj-exlimmpi  13148  uzdcinzz  13176  bj-2inf  13307  bj-peano4  13324  bj-nn0suc  13333  exmid1stab  13368  subctctexmid  13369  nninfalllem1  13378  nninfsellemqall  13386  nninfomnilem  13389  nninffeq  13391  exmidsbthrlem  13392  sbthomlem  13395  refeq  13398  isomninnlem  13400  apdifflemr  13415  redcwlpo  13422