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  623  simplimdc  860  mp3an3  1326  3impexpbicom  1438  mpisyl  1446  equcomi  1704  equsex  1728  equsexd  1729  spimt  1736  spimeh  1739  equvini  1758  equveli  1759  sbcof2  1810  dveeq2  1815  ax11v2  1820  ax16i  1858  pm13.183  2876  euxfr2dc  2923  sbcth  2977  sbcth2  3051  ssun3  3301  ssun4  3302  ralf0  3527  exmidexmid  4197  rext  4216  exss  4228  uniopel  4257  onsucelsucexmid  4530  suc11g  4557  eunex  4561  ordsoexmid  4562  tfisi  4587  finds1  4602  omsinds  4622  relop  4778  dmrnssfld  4891  iss  4954  relcoi1  5161  nfunv  5250  funimass2  5295  fvssunirng  5531  fvmptg  5593  oprabidlem  5906  fovcl  5980  elovmpo  6072  tfrlem1  6309  oaword1  6472  0domg  6837  diffifi  6894  exmidpw  6908  djulclb  7054  0ct  7106  nlt1pig  7340  dmaddpq  7378  dmmulpq  7379  archnqq  7416  prarloclemarch2  7418  prarloclemlt  7492  cnegex  8135  nnge1  8942  zneo  9354  fsum2d  11443  fsumabs  11473  fsumiun  11485  fprod2d  11631  efne0  11686  nn0o1gt2  11910  ennnfonelemex  12415  qtopbasss  14024  reeff1o  14197  coseq0negpitopi  14260  cos02pilt1  14275  logltb  14298  bdop  14630  bj-nntrans  14706