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  588  simplimdc  795  mp3an3  1262  3impexpbicom  1372  mpisyl  1380  equcomi  1637  equsex  1663  equsexd  1664  spimt  1671  spimeh  1674  equvini  1688  equveli  1689  sbcof2  1738  dveeq2  1743  ax11v2  1748  ax16i  1786  pm13.183  2752  euxfr2dc  2798  sbcth  2851  sbcth2  2924  ssun3  3163  ssun4  3164  ralf0  3381  exmidexmid  4022  rext  4033  exss  4045  uniopel  4074  onsucelsucexmid  4336  suc11g  4363  eunex  4367  ordsoexmid  4368  tfisi  4392  finds1  4407  omsinds  4425  relop  4574  dmrnssfld  4684  iss  4745  relcoi1  4949  nfunv  5033  funimass2  5078  fvssunirng  5304  fvmptg  5364  oprabidlem  5662  fovcl  5732  elovmpt2  5827  tfrlem1  6055  oaword1  6214  0domg  6533  diffifi  6590  exmidpw  6604  djulclb  6726  nlt1pig  6879  dmaddpq  6917  dmmulpq  6918  archnqq  6955  prarloclemarch2  6957  prarloclemlt  7031  cnegex  7639  nnge1  8417  zneo  8817  fsum2d  10792  fsumabs  10822  fsumiun  10833  nn0o1gt2  10998  bdop  11423  bj-nntrans  11503