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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  mp2  16  syl6mpi  63  mp2ani  422  pm2.24i  585  simplimdc  790  mp3an3  1257  3impexpbicom  1367  mpisyl  1375  equcomi  1632  equsex  1656  equsexd  1657  spimt  1664  spimeh  1667  equvini  1681  equveli  1682  sbcof2  1731  dveeq2  1736  ax11v2  1741  ax16i  1779  pm13.183  2732  euxfr2dc  2777  sbcth  2828  sbcth2  2901  ssun3  3137  ssun4  3138  ralf0  3344  rext  3970  exss  3982  uniopel  4011  onsucelsucexmid  4273  suc11g  4300  eunex  4304  ordsoexmid  4305  tfisi  4328  finds1  4343  relop  4504  dmrnssfld  4613  iss  4674  relcoi1  4869  nfunv  4953  funimass2  4997  fvssunirng  5210  fvmptg  5269  oprabidlem  5556  fovcl  5626  elovmpt2  5721  tfrlem1  5946  oaword1  6073  diffifi  6378  nlt1pig  6531  dmaddpq  6569  dmmulpq  6570  archnqq  6607  prarloclemarch2  6609  prarloclemlt  6683  cnegex  7286  nnge1  8062  zneo  8448  nn0o1gt2  10305  bdop  10666  bj-nntrans  10746