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  628  simplimdc  867  mp3an3  1362  3impexpbicom  1483  mpisyl  1491  equcomi  1752  equsex  1776  equsexd  1777  spimt  1784  spimeh  1787  equvini  1806  equveli  1807  sbcof2  1858  dveeq2  1863  ax11v2  1868  ax16i  1906  pm13.183  2944  euxfr2dc  2991  sbcth  3045  sbcth2  3120  ssun3  3372  ssun4  3373  ralf0  3597  exmidexmid  4286  rext  4307  exss  4319  uniopel  4349  onsucelsucexmid  4628  suc11g  4655  eunex  4659  ordsoexmid  4660  tfisi  4685  finds1  4700  omsinds  4720  relop  4880  dmrnssfld  4995  iss  5059  relcoi1  5268  nfunv  5359  funimass2  5408  fvssunirng  5654  fvmptg  5722  oprabidlem  6049  elovmpo  6221  tfrlem1  6474  oaword1  6639  modom  6994  0domg  7023  1ndom2  7051  diffifi  7083  exmidpw  7100  djulclb  7254  0ct  7306  iftrueb01  7441  nlt1pig  7561  dmaddpq  7599  dmmulpq  7600  archnqq  7637  prarloclemarch2  7639  prarloclemlt  7713  cnegex  8357  nnge1  9166  zneo  9581  fsum2d  11997  fsumabs  12027  fsumiun  12039  fprod2d  12185  efne0  12240  nn0o1gt2  12467  ennnfonelemex  13036  qtopbasss  15247  ivthdichlem  15377  dvmptfsum  15451  reeff1o  15499  coseq0negpitopi  15562  cos02pilt1  15577  logltb  15600  gausslemma2dlem0i  15788  2lgs  15835  bdop  16473  bj-nntrans  16549