Theorem mpi 15

Description: A nested modus ponens inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.)

Hypotheses

Ref	Expression
mpi.1	⊢ 𝜓
mpi.2	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
mpi	⊢ (𝜑 → 𝜒)

Proof of Theorem mpi

Step	Hyp	Ref	Expression
1		mpi.1	. . 3 ⊢ 𝜓
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝜓)
3		mpi.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	mpd 13	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mp2  16  syl6mpi  64  mp2ani  436  pm2.24i  632  simplimdc  872  mp3an3  1367  3impexpbicom  1488  mpisyl  1496  equcomi  1756  equsex  1780  equsexd  1782  spimt  1789  spimeh  1792  equvini  1811  equveli  1812  sbcof2  1863  dveeq2  1868  ax11v2  1873  ax16i  1911  pm13.183  2964  euxfr2dc  3011  sbcth  3065  sbcth2  3140  ssun3  3394  ssun4  3395  ralf0  3630  exmidexmid  4333  rext  4355  exss  4367  uniopel  4397  onsucelsucexmid  4677  suc11g  4704  eunex  4708  ordsoexmid  4709  tfisi  4734  finds1  4749  omsinds  4769  relop  4930  dmrnssfld  5045  iss  5109  relcoi1  5319  nfunv  5410  funimass2  5459  fvssunirng  5710  fvmptg  5781  oprabidlem  6116  elovmpo  6288  tfrlem1  6579  oaword1  6744  modom  7108  0domg  7137  1ndom2  7166  diffifi  7198  exmidpw  7215  djulclb  7395  0ct  7447  iftrueb01  7582  nlt1pig  7708  dmaddpq  7746  dmmulpq  7747  archnqq  7784  prarloclemarch2  7786  prarloclemlt  7860  cnegex  8505  nnge1  9329  zneo  9751  resq01  11108  fsum2d  12218  fsumabs  12248  fsumiun  12260  fprod2d  12406  efne0  12461  nn0o1gt2  12688  ennnfonelemex  13354  qtopbasss  15671  ivthdichlem  15801  dvmptfsum  15875  reeff1o  15923  coseq0negpitopi  15987  cos02pilt1  16002  logltb  16026  pellexlem3  16150  gausslemma2dlem0i  16274  2lgs  16321  bdop  16999  bj-nntrans  17075  exmidcon  17135