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	|- ps
mpi.2	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
mpi	|- ( ph -> ch )

Proof of Theorem mpi

Step	Hyp	Ref	Expression
1		mpi.1	. . 3 |- ps
2	1	a1i 9	. 2 |- ( ph -> ps )
3		mpi.2	. 2 |- ( ph -> ( ps -> ch ) )
4	2, 3	mpd 13	1 |- ( ph -> ch )

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  624  simplimdc  861  mp3an3  1337  3impexpbicom  1449  mpisyl  1457  equcomi  1715  equsex  1739  equsexd  1740  spimt  1747  spimeh  1750  equvini  1769  equveli  1770  sbcof2  1821  dveeq2  1826  ax11v2  1831  ax16i  1869  pm13.183  2890  euxfr2dc  2937  sbcth  2991  sbcth2  3065  ssun3  3315  ssun4  3316  ralf0  3541  exmidexmid  4211  rext  4230  exss  4242  uniopel  4271  onsucelsucexmid  4544  suc11g  4571  eunex  4575  ordsoexmid  4576  tfisi  4601  finds1  4616  omsinds  4636  relop  4792  dmrnssfld  4905  iss  4968  relcoi1  5175  nfunv  5265  funimass2  5310  fvssunirng  5546  fvmptg  5609  oprabidlem  5923  elovmpo  6091  tfrlem1  6328  oaword1  6491  0domg  6856  diffifi  6913  exmidpw  6927  djulclb  7074  0ct  7126  nlt1pig  7360  dmaddpq  7398  dmmulpq  7399  archnqq  7436  prarloclemarch2  7438  prarloclemlt  7512  cnegex  8155  nnge1  8962  zneo  9374  fsum2d  11463  fsumabs  11493  fsumiun  11505  fprod2d  11651  efne0  11706  nn0o1gt2  11930  ennnfonelemex  12440  qtopbasss  14425  reeff1o  14598  coseq0negpitopi  14661  cos02pilt1  14676  logltb  14699  bdop  15031  bj-nntrans  15107