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

Syntax hints:   → wi 4

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

This theorem is referenced by:  mp2  16  syl6mpi  64  mp2ani  432  pm2.24i  626  simplimdc  865  mp3an3  1360  3impexpbicom  1481  mpisyl  1489  equcomi  1750  equsex  1774  equsexd  1775  spimt  1782  spimeh  1785  equvini  1804  equveli  1805  sbcof2  1856  dveeq2  1861  ax11v2  1866  ax16i  1904  pm13.183  2942  euxfr2dc  2989  sbcth  3043  sbcth2  3118  ssun3  3370  ssun4  3371  ralf0  3595  exmidexmid  4284  rext  4305  exss  4317  uniopel  4347  onsucelsucexmid  4626  suc11g  4653  eunex  4657  ordsoexmid  4658  tfisi  4683  finds1  4698  omsinds  4718  relop  4878  dmrnssfld  4993  iss  5057  relcoi1  5266  nfunv  5357  funimass2  5405  fvssunirng  5650  fvmptg  5718  oprabidlem  6044  elovmpo  6216  tfrlem1  6469  oaword1  6634  modom  6989  0domg  7018  1ndom2  7046  diffifi  7076  exmidpw  7093  djulclb  7245  0ct  7297  iftrueb01  7431  nlt1pig  7551  dmaddpq  7589  dmmulpq  7590  archnqq  7627  prarloclemarch2  7629  prarloclemlt  7703  cnegex  8347  nnge1  9156  zneo  9571  fsum2d  11986  fsumabs  12016  fsumiun  12028  fprod2d  12174  efne0  12229  nn0o1gt2  12456  ennnfonelemex  13025  qtopbasss  15235  ivthdichlem  15365  dvmptfsum  15439  reeff1o  15487  coseq0negpitopi  15550  cos02pilt1  15565  logltb  15588  gausslemma2dlem0i  15776  2lgs  15823  bdop  16406  bj-nntrans  16482