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  2898  euxfr2dc  2945  sbcth  2999  sbcth2  3073  ssun3  3324  ssun4  3325  ralf0  3549  exmidexmid  4225  rext  4244  exss  4256  uniopel  4285  onsucelsucexmid  4562  suc11g  4589  eunex  4593  ordsoexmid  4594  tfisi  4619  finds1  4634  omsinds  4654  relop  4812  dmrnssfld  4925  iss  4988  relcoi1  5197  nfunv  5287  funimass2  5332  fvssunirng  5569  fvmptg  5633  oprabidlem  5949  elovmpo  6117  tfrlem1  6361  oaword1  6524  0domg  6893  diffifi  6950  exmidpw  6964  djulclb  7114  0ct  7166  nlt1pig  7401  dmaddpq  7439  dmmulpq  7440  archnqq  7477  prarloclemarch2  7479  prarloclemlt  7553  cnegex  8197  nnge1  9005  zneo  9418  fsum2d  11578  fsumabs  11608  fsumiun  11620  fprod2d  11766  efne0  11821  nn0o1gt2  12046  ennnfonelemex  12571  qtopbasss  14689  ivthdichlem  14805  reeff1o  14908  coseq0negpitopi  14971  cos02pilt1  14986  logltb  15009  gausslemma2dlem0i  15173  bdop  15367  bj-nntrans  15443