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  32  mpdd  36  mp2d  41  pm2.43i  43  syl3c  57  mpbid  135  mpbird  156  jcai  294  mp2and  409  pm2.21dd  550  mt2d  555  mpjaod  637  impidc  754  jadc  759  pm2.54dc  789  stabtestimpdc  823  pm4.55dc  845  oplem1  881  xor3dc  1275  exlimdd  1749  exlimddv  1775  eqrdav  2036  necon1aidc  2250  necon1bidc  2251  necon4aidc  2267  rexlimddv  2431  vtoclgft  2598  sseldd  2940  ssneldd  2942  tpid3g  3474  preq12b  3532  axpweq  3915  opth  3965  issod  4047  ralxfr2d  4162  rexxfr2d  4163  eldifpw  4174  onun2  4182  onuni  4186  elirr  4224  en2lp  4232  peano2  4261  relop  4429  elres  4589  sotri2  4665  iota4an  4829  iota5  4830  funeu  4869  funopg  4877  imadiflem  4921  funimaexglem  4925  ssimaex  5177  ffvelrn  5243  dff3im  5255  dffo4  5258  f1eqcocnv  5374  f1oiso2  5409  riota5f  5435  riotass2  5437  acexmidlemcase  5450  ovmpt2df  5574  ovmpt2dv2  5576  ovi3  5579  ov6g  5580  caoftrn  5678  op1steq  5747  tfr0  5878  tfrlemibxssdm  5882  tfrlemi14d  5888  rdgivallem  5908  frecsuclem3  5929  freccl  5932  nnsucelsuc  6009  nnsucsssuc  6010  nnawordex  6037  ersym  6054  fundmen  6222  elni2  6298  mulclpi  6312  nlt1pig  6325  indpi  6326  recclnq  6376  ltexnqq  6391  halfnqq  6393  prarloclemarch  6401  prarloclemarch2  6402  prop  6458  prltlu  6470  prarloclem3step  6479  prarloclem5  6483  prarloclem  6484  prarloc  6486  prarloc2  6487  genpml  6500  genpmu  6501  genprndl  6504  genprndu  6505  genpdisj  6506  addnqprllem  6510  addnqprulem  6511  addlocprlemeq  6516  addlocprlemgt  6517  addlocprlem  6518  addlocpr  6519  nqprloc  6528  nqprl  6533  addnqprlemrl  6538  addnqprlemru  6539  appdivnq  6544  prmuloc  6547  prmuloc2  6548  mullocprlem  6551  mullocpr  6552  ltprordil  6565  ltpopr  6569  ltsopr  6570  ltaddpr  6571  ltexprlemm  6574  ltexprlemopl  6575  ltexprlemlol  6576  ltexprlemopu  6577  ltexprlemupu  6578  ltexprlemloc  6581  ltexprlemfl  6583  ltexprlemrl  6584  ltexprlemfu  6585  ltexprlemru  6586  ltaprg  6592  recexprlemm  6596  recexprlem1ssl  6605  recexprlem1ssu  6606  aptiprleml  6611  aptiprlemu  6612  archpr  6615  cauappcvgprlemm  6617  cauappcvgprlemopl  6618  cauappcvgprlemlol  6619  cauappcvgprlemopu  6620  cauappcvgprlemupu  6621  cauappcvgprlemdisj  6623  cauappcvgprlemloc  6624  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  cauappcvgprlemladdru  6628  cauappcvgprlem1  6631  caucvgprlemnkj  6637  caucvgprlemnbj  6638  caucvgprlemm  6639  caucvgprlemopl  6640  caucvgprlemlol  6641  caucvgprlemopu  6642  caucvgprlemupu  6643  caucvgprlemdisj  6645  caucvgprlemloc  6646  caucvgprlemladdfu  6648  caucvgprlem1  6650  caucvgprlemlim  6652  recexgt0sr  6701  mulgt0sr  6704  archsr  6708  axarch  6773  lelttr  6903  ltletr  6904  ltled  6932  cnegexlem1  6983  cnegexlem2  6984  renegcl  7068  gt0add  7357  apreap  7371  apirr  7389  apsym  7390  apcotr  7391  apadd1  7392  apneg  7395  mulext1  7396  mulap0r  7399  apti  7406  recexap  7416  mulap0  7417  receuap  7432  lep1  7592  lem1  7594  letrp1  7595  recreclt  7647  nnrecgt0  7732  bndndx  7956  nn0ge2m1nn  8018  elnn0z  8034  peano2z  8057  zaddcl  8061  ztri3or0  8063  zltnle  8067  zdceq  8092  zdcle  8093  zdclt  8094  zdiv  8104  zeo  8119  fnn0ind  8130  btwnz  8133  uzm1  8279  uzp1  8282  indstr  8312  eluzdc  8323  nn01to3  8328  qapne  8350  xrlelttr  8492  xrltletr  8493  ge0nemnf  8507  fzdcel  8674  elfzouz2  8787  fzoss1  8797  fzospliti  8802  fzocatel  8825  fzostep1  8863  frec2uzzd  8867  frec2uzuzd  8869  frec2uzlt2d  8871  frec2uzf1od  8873  frecuzrdgrrn  8875  frecuzrdgcl  8880  frecuzrdgsuc  8882  iseqval  8900  iseqfveq2  8905  expgt1  8947  expnbnd  9025  expnlbnd2  9027  cjap  9134  bj-exlimmpi  9245  bj-2inf  9397  bj-peano4  9415  bj-nn0suc  9424