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  1322  xor3dc  1369  exlimdd  1852  exlimddv  1878  eqrdav  2156  necon1aidc  2378  necon1bidc  2379  necon4aidc  2395  reximddv  2560  reximssdv  2561  rexlimddv  2579  vtoclgft  2762  rspcedvd  2822  sseldd  3129  ssneldd  3131  tpid3g  3674  preq12b  3733  axpweq  4132  exmid1dc  4161  opth  4197  issod  4279  frirrg  4310  frind  4312  ralxfr2d  4424  rexxfr2d  4425  eldifpw  4437  onun2  4449  onuni  4453  elirr  4500  en2lp  4513  wetriext  4536  peano2  4554  relop  4736  elres  4902  sotri2  4983  iota4an  5154  iota5  5155  funeu  5195  funopg  5204  imadiflem  5249  funimaexglem  5253  ssimaex  5529  ffvelrn  5600  dff3im  5612  dffo4  5615  f1eqcocnv  5741  f1oiso2  5777  riota5f  5804  riotass2  5806  acexmidlemcase  5819  ovmpodf  5952  ovmpodv2  5954  ovi3  5957  ov6g  5958  caoftrn  6057  op1steq  6127  tfr0dm  6269  tfrlemibxssdm  6274  tfrlemi14d  6280  tfr1onlembxssdm  6290  tfr1onlemaccex  6295  tfr1onlemres  6296  tfrcllembxssdm  6303  tfrcllemaccex  6308  tfrcllemres  6309  rdgivallem  6328  nnsucelsuc  6438  nnsucsssuc  6439  dcdifsnid  6451  nnawordex  6475  ersym  6492  mapvalg  6603  pmvalg  6604  mapsn  6635  fundmen  6751  mapdom1g  6792  fidceq  6814  fin0or  6831  findcard2  6834  findcard2s  6835  fiintim  6873  suplub2ti  6945  supsnti  6949  supisoex  6953  difinfsnlem  7043  difinfsn  7044  ctm  7053  ctssdclemn0  7054  ctssdccl  7055  ctssdc  7057  enumctlemm  7058  nnnninfeq2  7072  enomnilem  7081  exmidomniim  7084  exmidomni  7085  fodjuomnilemdc  7087  fodjuomnilemres  7091  omnimkv  7099  mkvprop  7101  omniwomnimkv  7110  en2eleq  7130  acfun  7142  exmidontriimlem1  7156  exmidontriimlem4  7159  exmidontriim  7160  ccfunen  7184  cc4f  7189  cc4n  7191  elni2  7234  mulclpi  7248  nlt1pig  7261  indpi  7262  recclnq  7312  ltexnqq  7328  halfnqq  7330  prarloclemarch  7338  prarloclemarch2  7339  prop  7395  prltlu  7407  prarloclem3step  7416  prarloclem5  7420  prarloclem  7421  prarloc  7423  prarloc2  7424  genpml  7437  genpmu  7438  genprndl  7441  genprndu  7442  genpdisj  7443  addnqprllem  7447  addnqprulem  7448  addlocprlemeq  7453  addlocprlemgt  7454  addlocprlem  7455  addlocpr  7456  nqprloc  7465  nqprl  7471  nqpru  7472  addnqprlemrl  7477  addnqprlemru  7478  appdivnq  7483  prmuloc  7486  prmuloc2  7487  mullocprlem  7490  mullocpr  7491  mulnqprlemrl  7493  mulnqprlemru  7494  ltprordil  7509  ltpopr  7515  ltsopr  7516  ltaddpr  7517  ltexprlemm  7520  ltexprlemopl  7521  ltexprlemlol  7522  ltexprlemopu  7523  ltexprlemupu  7524  ltexprlemloc  7527  ltexprlemfl  7529  ltexprlemrl  7530  ltexprlemfu  7531  ltexprlemru  7532  ltaprg  7539  recexprlemm  7544  recexprlem1ssl  7553  recexprlem1ssu  7554  aptiprleml  7559  aptiprlemu  7560  archpr  7563  cauappcvgprlemm  7565  cauappcvgprlemopl  7566  cauappcvgprlemlol  7567  cauappcvgprlemopu  7568  cauappcvgprlemupu  7569  cauappcvgprlemdisj  7571  cauappcvgprlemloc  7572  cauappcvgprlemladdfu  7574  cauappcvgprlemladdfl  7575  cauappcvgprlemladdru  7576  cauappcvgprlem1  7579  archrecpr  7584  caucvgprlemnkj  7586  caucvgprlemnbj  7587  caucvgprlemm  7588  caucvgprlemopl  7589  caucvgprlemlol  7590  caucvgprlemopu  7591  caucvgprlemupu  7592  caucvgprlemdisj  7594  caucvgprlemloc  7595  caucvgprlemladdfu  7597  caucvgprlem1  7599  caucvgprlemlim  7601  caucvgprprlemnbj  7613  caucvgprprlemml  7614  caucvgprprlemopl  7617  caucvgprprlemlol  7618  caucvgprprlemopu  7619  caucvgprprlemupu  7620  caucvgprprlemdisj  7622  caucvgprprlemloc  7623  caucvgprprlemexbt  7626  caucvgprprlemaddq  7628  caucvgprprlemlim  7631  suplocexprlemss  7635  suplocexprlemrl  7637  suplocexprlemmu  7638  suplocexprlemru  7639  suplocexprlemdisj  7640  suplocexprlemloc  7641  suplocexprlemub  7643  suplocexprlemlub  7644  recexgt0sr  7693  mulgt0sr  7698  archsr  7702  caucvgsrlemoffcau  7718  suplocsrlemb  7726  suplocsrlempr  7727  suplocsrlem  7728  cnm  7752  axarch  7811  axcaucvglemcau  7818  axpre-suploclemres  7821  lelttr  7965  ltletr  7966  ltled  7994  cnegexlem1  8050  cnegexlem2  8051  renegcl  8136  negf1o  8257  gt0add  8448  apreap  8462  apirr  8480  apsym  8481  apcotr  8482  apadd1  8483  apneg  8486  mulext1  8487  mulap0r  8490  apti  8497  aprcl  8521  recexap  8527  mulap0  8528  receuap  8543  mul0eqap  8544  lep1  8716  lem1  8718  letrp1  8719  recreclt  8771  lbinf  8819  suprubex  8822  nnrecgt0  8871  bndndx  9089  nn0ge2m1nn  9150  elnn0z  9180  peano2z  9203  zaddcl  9207  ztri3or0  9209  zltnle  9213  zdceq  9239  zdcle  9240  zdclt  9241  zdiv  9252  zeo  9269  fnn0ind  9280  btwnz  9283  uzm1  9469  uzp1  9472  indstr  9504  supinfneg  9506  infsupneg  9507  eluzdc  9521  nn01to3  9526  qapne  9548  xrltled  9706  xrlelttr  9710  xrltletr  9711  ge0nemnf  9728  fzdcel  9942  elfzouz2  10060  fzoss1  10070  fzospliti  10075  fzocatel  10098  fzostep1  10136  qtri3or  10142  qltnle  10145  qdceq  10146  exbtwnzlemex  10149  rebtwn2zlemstep  10152  rebtwn2z  10154  qbtwnxr  10157  ioom  10160  ico0  10161  ioc0  10162  flqeqceilz  10217  modqadd1  10260  modqmul1  10276  frec2uzuzd  10301  frec2uzlt2d  10303  frec2uzf1od  10305  frecuzrdgrrn  10307  frec2uzrdg  10308  frecuzrdgrcl  10309  frecuzrdgsuc  10313  frecuzrdgrclt  10314  frecuzrdgdomlem  10316  uzsinds  10341  seqvalcd  10358  seqovcd  10362  seq3fveq2  10368  seq3shft2  10372  monoord  10375  seq3split  10378  seq3caopr3  10380  iseqf1olemab  10388  iseqf1olemnanb  10389  iseqf1olemqk  10393  seq3id3  10406  seq3id2  10408  seq3homo  10409  expgt1  10457  m1expeven  10466  expnbnd  10541  expnlbnd2  10543  apexp1  10592  hashennn  10654  zfz1isolem1  10711  seq3coll  10713  cjap  10806  caucvgre  10881  cvg1nlemres  10885  resqrexlemgt0  10920  resqrexlemglsq  10922  resqrexlemga  10923  resqrtcl  10929  abslt  10988  abssubap0  10990  abssubne0  10991  caubnd2  11017  qdenre  11102  maxabslemlub  11107  maxabs  11109  maxleast  11113  fimaxre2  11126  xrmaxiflemlub  11145  xrmaxif  11148  xrmaxltsup  11155  xrmaxadd  11158  xrmineqinf  11166  climuni  11190  2clim  11198  climcn1  11205  climcn2  11206  subcn2  11208  mulcn2  11209  climsqz  11232  climsqz2  11233  climcau  11244  climcvg1nlem  11246  climcaucn  11248  serf0  11249  sumrbdclem  11274  summodclem2  11279  zsumdc  11281  divcnv  11394  absltap  11406  absgtap  11407  mertenslem2  11433  ntrivcvgap  11445  prodrbdclem  11468  prodmodclem2  11474  zproddc  11476  prodssdc  11486  fprodsplitdc  11493  fprodcl2lem  11502  efcllemp  11555  tanvalap  11605  sin01bnd  11654  cos01bnd  11655  sin01gt0  11658  absef  11666  eirrap  11674  dvds0  11701  dvdsmul1  11708  dvdsmultr1d  11725  dvdslelemd  11734  divconjdvds  11740  alzdvds  11745  sqoddm1div8z  11776  nno  11796  divalglemex  11812  zsupcllemstep  11831  zsupcl  11833  infssuzledc  11836  dvdsbnd  11839  dvdslegcd  11847  zeqzmulgcd  11853  gcd0id  11862  gcdaddm  11867  gcd1  11870  gcdabs  11871  bezoutlemnewy  11879  bezoutlemstep  11880  bezoutlemmain  11881  bezoutlemex  11884  bezoutlemzz  11885  bezoutlemaz  11886  bezoutlembz  11887  bezoutlembi  11888  bezoutlemle  11891  bezoutlemsup  11892  mulgcd  11899  gcdzeq  11905  dvdsmulgcd  11908  sqgcd  11912  bezoutr1  11916  algcvga  11927  algfx  11928  eucalglt  11933  eucalg  11935  lcmneg  11950  lcmabs  11952  lcmgcdlem  11953  ncoprmgcdne1b  11965  mulgcddvds  11970  qredeq  11972  divgcdcoprm0  11977  cncongr1  11979  isprm2lem  11992  nprm  11999  dvdsnprmd  12001  prmdvdsfz  12015  coprm  12018  isprm6  12021  sqrt2irr  12036  pw2dvdslemn  12039  pw2dvdseulemle  12041  oddpwdclemdvds  12044  oddpwdclemndvds  12045  sqrt2irrap  12054  qnumdencl  12061  prmdiv  12109  ennnfonelemex  12143  ennnfonelemhom  12144  ennnfonelemrnh  12145  ennnfonelemnn0  12151  ennnfonelemim  12153  exmidunben  12155  ctinfomlemom  12156  ctinfom  12157  ctinf  12159  omctfn  12172  nninfdclemp1  12181  tgcl  12464  neii1  12547  neii2  12549  neiss  12550  tpnei  12560  tgrest  12569  ssrest  12582  icnpimaex  12611  lmcvg  12617  cnpnei  12619  cnptopco  12622  lmff  12649  txcnp  12671  txcn  12675  hmeontr  12713  blssec  12838  mopni3  12884  blsscls2  12893  comet  12899  bdxmet  12901  bdmopn  12904  xmettxlem  12909  xmettx  12910  addcncntoplem  12951  mulc1cncf  12976  cncfco  12978  cncfmptc  12982  mulcncflem  12990  mulcncf  12991  dedekindeulemlu  12999  dedekindeulemeu  13000  suplociccreex  13002  suplociccex  13003  dedekindicclemlu  13008  dedekindicclemeu  13009  ivthinclemlopn  13014  ivthinclemlr  13015  ivthinclemuopn  13016  ivthinclemur  13017  ivthinclemloc  13019  ivthinc  13021  limcimolemlt  13033  limcresi  13035  cnplimcim  13036  cnplimclemle  13037  cnplimclemr  13038  limccnpcntop  13044  limccoap  13047  dvcoapbr  13071  dvcj  13073  efltlemlt  13095  sin0pilem2  13103  tangtx  13159  logdivlti  13202  rplogbval  13262  logbgcd1irraplemexp  13285  logbgcd1irraplemap  13286  logbgcd1irrap  13287  bj-exlimmpi  13344  uzdcinzz  13372  bj-charfundcALT  13384  bj-2inf  13513  bj-peano4  13530  bj-nn0suc  13539  exmid1stab  13572  subctctexmid  13573  nninfalllem1  13580  nninfsellemqall  13587  nninfomnilem  13590  nninffeq  13592  exmidsbthrlem  13593  sbthomlem  13596  refeq  13599  isomninnlem  13601  apdifflemr  13618  redcwlpo  13626  reap0  13629  nconstwlpolem  13635