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

This theorem is referenced by:  mp2  16  syl6mpi  63  mp2ani  423  pm2.24i  586  simplimdc  791  mp3an3  1258  3impexpbicom  1368  mpisyl  1376  equcomi  1633  equsex  1657  equsexd  1658  spimt  1665  spimeh  1668  equvini  1682  equveli  1683  sbcof2  1732  dveeq2  1737  ax11v2  1742  ax16i  1780  pm13.183  2733  euxfr2dc  2778  sbcth  2829  sbcth2  2902  ssun3  3138  ssun4  3139  ralf0  3352  rext  3978  exss  3990  uniopel  4019  onsucelsucexmid  4281  suc11g  4308  eunex  4312  ordsoexmid  4313  tfisi  4336  finds1  4351  relop  4514  dmrnssfld  4623  iss  4684  relcoi1  4879  nfunv  4963  funimass2  5008  fvssunirng  5221  fvmptg  5280  oprabidlem  5567  fovcl  5637  elovmpt2  5732  tfrlem1  5957  oaword1  6115  diffifi  6428  nlt1pig  6593  dmaddpq  6631  dmmulpq  6632  archnqq  6669  prarloclemarch2  6671  prarloclemlt  6745  cnegex  7353  nnge1  8129  zneo  8529  nn0o1gt2  10449  bdop  10824  bj-nntrans  10904