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 7	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-2 6  ax-mp 7

This theorem is referenced by:  syl  14  mpi  15  id  19  mpcom  36  mpdd  40  mp2d  46  pm2.43i  48  syl3c  62  mpbid  145  mpbird  165  jcai  304  mp2and  423  pm2.21dd  582  mt2d  587  mpjaod  670  impidc  788  jadc  793  pm2.54dc  823  stabtestimpdc  857  pm4.55dc  879  oplem1  916  mp3and  1271  xor3dc  1318  exlimdd  1793  exlimddv  1819  eqrdav  2080  necon1aidc  2296  necon1bidc  2297  necon4aidc  2313  reximddv  2464  rexlimddv  2481  vtoclgft  2649  rspcdva  2707  rspcedvd  2708  sseldd  3000  ssneldd  3002  tpid3g  3505  preq12b  3562  axpweq  3945  opth  3992  issod  4074  frirrg  4105  frind  4107  ralxfr2d  4214  rexxfr2d  4215  eldifpw  4226  onun2  4234  onuni  4238  elirr  4284  en2lp  4297  wetriext  4319  peano2  4336  relop  4504  elres  4664  sotri2  4742  iota4an  4906  iota5  4907  funeu  4946  funopg  4954  imadiflem  4998  funimaexglem  5002  ssimaex  5255  ffvelrn  5321  dff3im  5333  dffo4  5336  f1eqcocnv  5451  f1oiso2  5486  riota5f  5512  riotass2  5514  acexmidlemcase  5527  ovmpt2df  5652  ovmpt2dv2  5654  ovi3  5657  ov6g  5658  caoftrn  5756  op1steq  5825  tfr0  5960  tfrlemibxssdm  5964  tfrlemi14d  5970  rdgivallem  5991  frecsuclem3  6013  freccl  6016  nnsucelsuc  6093  nnsucsssuc  6094  nnawordex  6124  ersym  6141  fundmen  6309  fidceq  6354  fin0or  6370  findcard2  6373  findcard2s  6374  suplub2ti  6414  supsnti  6418  supisoex  6422  elni2  6504  mulclpi  6518  nlt1pig  6531  indpi  6532  recclnq  6582  ltexnqq  6598  halfnqq  6600  prarloclemarch  6608  prarloclemarch2  6609  prop  6665  prltlu  6677  prarloclem3step  6686  prarloclem5  6690  prarloclem  6691  prarloc  6693  prarloc2  6694  genpml  6707  genpmu  6708  genprndl  6711  genprndu  6712  genpdisj  6713  addnqprllem  6717  addnqprulem  6718  addlocprlemeq  6723  addlocprlemgt  6724  addlocprlem  6725  addlocpr  6726  nqprloc  6735  nqprl  6741  nqpru  6742  addnqprlemrl  6747  addnqprlemru  6748  appdivnq  6753  prmuloc  6756  prmuloc2  6757  mullocprlem  6760  mullocpr  6761  mulnqprlemrl  6763  mulnqprlemru  6764  ltprordil  6779  ltpopr  6785  ltsopr  6786  ltaddpr  6787  ltexprlemm  6790  ltexprlemopl  6791  ltexprlemlol  6792  ltexprlemopu  6793  ltexprlemupu  6794  ltexprlemloc  6797  ltexprlemfl  6799  ltexprlemrl  6800  ltexprlemfu  6801  ltexprlemru  6802  ltaprg  6809  recexprlemm  6814  recexprlem1ssl  6823  recexprlem1ssu  6824  aptiprleml  6829  aptiprlemu  6830  archpr  6833  cauappcvgprlemm  6835  cauappcvgprlemopl  6836  cauappcvgprlemlol  6837  cauappcvgprlemopu  6838  cauappcvgprlemupu  6839  cauappcvgprlemdisj  6841  cauappcvgprlemloc  6842  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  cauappcvgprlemladdru  6846  cauappcvgprlem1  6849  archrecpr  6854  caucvgprlemnkj  6856  caucvgprlemnbj  6857  caucvgprlemm  6858  caucvgprlemopl  6859  caucvgprlemlol  6860  caucvgprlemopu  6861  caucvgprlemupu  6862  caucvgprlemdisj  6864  caucvgprlemloc  6865  caucvgprlemladdfu  6867  caucvgprlem1  6869  caucvgprlemlim  6871  caucvgprprlemnbj  6883  caucvgprprlemml  6884  caucvgprprlemopl  6887  caucvgprprlemlol  6888  caucvgprprlemopu  6889  caucvgprprlemupu  6890  caucvgprprlemdisj  6892  caucvgprprlemloc  6893  caucvgprprlemexbt  6896  caucvgprprlemaddq  6898  caucvgprprlemlim  6901  recexgt0sr  6950  mulgt0sr  6954  archsr  6958  caucvgsrlemoffcau  6974  axarch  7057  axcaucvglemcau  7064  lelttr  7199  ltletr  7200  ltled  7228  cnegexlem1  7283  cnegexlem2  7284  renegcl  7369  negf1o  7486  gt0add  7673  apreap  7687  apirr  7705  apsym  7706  apcotr  7707  apadd1  7708  apneg  7711  mulext1  7712  mulap0r  7715  apti  7722  recexap  7743  mulap0  7744  receuap  7759  lep1  7923  lem1  7925  letrp1  7926  recreclt  7978  lbinf  8026  suprubex  8029  nnrecgt0  8076  bndndx  8287  nn0ge2m1nn  8348  elnn0z  8364  peano2z  8387  zaddcl  8391  ztri3or0  8393  zltnle  8397  zdceq  8423  zdcle  8424  zdclt  8425  zdiv  8435  zeo  8452  fnn0ind  8463  btwnz  8466  uzm1  8649  uzp1  8652  indstr  8681  supinfneg  8683  infsupneg  8684  eluzdc  8697  nn01to3  8702  qapne  8724  xrlelttr  8876  xrltletr  8877  ge0nemnf  8891  fzdcel  9059  elfzouz2  9170  fzoss1  9180  fzospliti  9185  fzocatel  9208  fzostep1  9246  qtri3or  9252  qltnle  9255  qdceq  9256  qbtwnzlemex  9259  rebtwn2zlemstep  9261  rebtwn2z  9263  qbtwnxr  9266  ioom  9269  ico0  9270  ioc0  9271  flqeqceilz  9320  modqadd1  9363  modqmul1  9379  frec2uzzd  9402  frec2uzuzd  9404  frec2uzlt2d  9406  frec2uzf1od  9408  frecuzrdgrrn  9410  frecuzrdgcl  9415  frecuzrdgsuc  9417  uzsinds  9428  iseqval  9440  iseqss  9446  iseqfveq2  9448  iseqshft2  9452  monoord  9455  iseqsplit  9458  iseqcaopr3  9460  iseqid3s  9466  iseqhomo  9468  expgt1  9514  m1expeven  9523  expnbnd  9596  expnlbnd2  9598  cjap  9793  caucvgre  9867  cvg1nlemres  9871  resqrexlemgt0  9906  resqrexlemglsq  9908  resqrexlemga  9909  resqrtcl  9915  abslt  9974  abssubap0  9976  abssubne0  9977  caubnd2  10003  qdenre  10088  maxabslemlub  10093  maxabs  10095  maxleast  10099  fimaxre2  10109  climuni  10132  2clim  10140  climcn1  10147  climcn2  10148  subcn2  10150  mulcn2  10151  climsqz  10173  climsqz2  10174  climcau  10184  climcvg1nlem  10186  climcaucn  10188  serif0  10189  dvds0  10210  dvdsmul1  10217  dvdsmultr1d  10234  dvdslelemd  10243  divconjdvds  10249  alzdvds  10254  sqoddm1div8z  10286  nno  10306  divalglemex  10322  zsupcllemstep  10341  zsupcl  10343  infssuzledc  10346  dvdsbnd  10348  dvdslegcd  10356  zeqzmulgcd  10362  gcd0id  10370  gcdaddm  10375  gcd1  10378  gcdabs  10379  bezoutlemnewy  10385  bezoutlemstep  10386  bezoutlemmain  10387  bezoutlemex  10390  bezoutlemzz  10391  bezoutlemaz  10392  bezoutlembz  10393  bezoutlembi  10394  bezoutlemle  10397  bezoutlemsup  10398  mulgcd  10405  gcdzeq  10411  dvdsmulgcd  10414  sqgcd  10418  bezoutr1  10422  ialgcvga  10433  ialgfx  10434  eucalglt  10439  eucialg  10441  lcmneg  10456  lcmabs  10458  lcmgcdlem  10459  ncoprmgcdne1b  10471  mulgcddvds  10476  qredeq  10478  divgcdcoprm0  10483  cncongr1  10485  isprm2lem  10498  nprm  10505  dvdsnprmd  10507  prmdvdsfz  10520  coprm  10523  isprm6  10526  sqrt2irr  10541  pw2dvdslemn  10543  pw2dvdseulemle  10545  oddpwdclemdvds  10548  oddpwdclemndvds  10549  sqrt2irrap  10558  bj-exlimmpi  10581  bj-2inf  10733  bj-peano4  10750  bj-nn0suc  10759