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  2899  euxfr2dc  2946  sbcth  3000  sbcth2  3074  ssun3  3325  ssun4  3326  ralf0  3550  exmidexmid  4226  rext  4245  exss  4257  uniopel  4286  onsucelsucexmid  4563  suc11g  4590  eunex  4594  ordsoexmid  4595  tfisi  4620  finds1  4635  omsinds  4655  relop  4813  dmrnssfld  4926  iss  4989  relcoi1  5198  nfunv  5288  funimass2  5333  fvssunirng  5570  fvmptg  5634  oprabidlem  5950  elovmpo  6119  tfrlem1  6363  oaword1  6526  0domg  6895  diffifi  6952  exmidpw  6966  djulclb  7116  0ct  7168  nlt1pig  7403  dmaddpq  7441  dmmulpq  7442  archnqq  7479  prarloclemarch2  7481  prarloclemlt  7555  cnegex  8199  nnge1  9007  zneo  9421  fsum2d  11581  fsumabs  11611  fsumiun  11623  fprod2d  11769  efne0  11824  nn0o1gt2  12049  ennnfonelemex  12574  qtopbasss  14700  ivthdichlem  14830  dvmptfsum  14904  reeff1o  14949  coseq0negpitopi  15012  cos02pilt1  15027  logltb  15050  gausslemma2dlem0i  15214  2lgs  15261  bdop  15437  bj-nntrans  15513