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  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  3627  exmidexmid  4328  rext  4350  exss  4362  uniopel  4392  onsucelsucexmid  4672  suc11g  4699  eunex  4703  ordsoexmid  4704  tfisi  4729  finds1  4744  omsinds  4764  relop  4925  dmrnssfld  5040  iss  5104  relcoi1  5314  nfunv  5405  funimass2  5454  fvssunirng  5705  fvmptg  5775  oprabidlem  6106  elovmpo  6278  tfrlem1  6569  oaword1  6734  modom  7098  0domg  7127  1ndom2  7156  diffifi  7188  exmidpw  7205  djulclb  7385  0ct  7437  iftrueb01  7572  nlt1pig  7698  dmaddpq  7736  dmmulpq  7737  archnqq  7774  prarloclemarch2  7776  prarloclemlt  7850  cnegex  8494  nnge1  9306  zneo  9726  resq01  11073  fsum2d  12180  fsumabs  12210  fsumiun  12222  fprod2d  12368  efne0  12423  nn0o1gt2  12650  ennnfonelemex  13283  qtopbasss  15545  ivthdichlem  15675  dvmptfsum  15749  reeff1o  15797  coseq0negpitopi  15860  cos02pilt1  15875  logltb  15898  pellexlem3  16007  gausslemma2dlem0i  16090  2lgs  16137  bdop  16815  bj-nntrans  16891  exmidcon  16950