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  1336  3impexpbicom  1448  mpisyl  1456  equcomi  1714  equsex  1738  equsexd  1739  spimt  1746  spimeh  1749  equvini  1768  equveli  1769  sbcof2  1820  dveeq2  1825  ax11v2  1830  ax16i  1868  pm13.183  2887  euxfr2dc  2934  sbcth  2988  sbcth2  3062  ssun3  3312  ssun4  3313  ralf0  3538  exmidexmid  4208  rext  4227  exss  4239  uniopel  4268  onsucelsucexmid  4541  suc11g  4568  eunex  4572  ordsoexmid  4573  tfisi  4598  finds1  4613  omsinds  4633  relop  4789  dmrnssfld  4902  iss  4965  relcoi1  5172  nfunv  5261  funimass2  5306  fvssunirng  5542  fvmptg  5605  oprabidlem  5919  fovcl  5993  elovmpo  6085  tfrlem1  6322  oaword1  6485  0domg  6850  diffifi  6907  exmidpw  6921  djulclb  7067  0ct  7119  nlt1pig  7353  dmaddpq  7391  dmmulpq  7392  archnqq  7429  prarloclemarch2  7431  prarloclemlt  7505  cnegex  8148  nnge1  8955  zneo  9367  fsum2d  11456  fsumabs  11486  fsumiun  11498  fprod2d  11644  efne0  11699  nn0o1gt2  11923  ennnfonelemex  12428  qtopbasss  14292  reeff1o  14465  coseq0negpitopi  14528  cos02pilt1  14543  logltb  14566  bdop  14898  bj-nntrans  14974