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  862  mp3an3  1339  3impexpbicom  1459  mpisyl  1467  equcomi  1728  equsex  1752  equsexd  1753  spimt  1760  spimeh  1763  equvini  1782  equveli  1783  sbcof2  1834  dveeq2  1839  ax11v2  1844  ax16i  1882  pm13.183  2918  euxfr2dc  2965  sbcth  3019  sbcth2  3094  ssun3  3346  ssun4  3347  ralf0  3571  exmidexmid  4256  rext  4277  exss  4289  uniopel  4319  onsucelsucexmid  4596  suc11g  4623  eunex  4627  ordsoexmid  4628  tfisi  4653  finds1  4668  omsinds  4688  relop  4846  dmrnssfld  4960  iss  5024  relcoi1  5233  nfunv  5323  funimass2  5371  fvssunirng  5614  fvmptg  5678  oprabidlem  5998  elovmpo  6168  tfrlem1  6417  oaword1  6580  0domg  6959  1ndom2  6987  diffifi  7017  exmidpw  7031  djulclb  7183  0ct  7235  iftrueb01  7369  nlt1pig  7489  dmaddpq  7527  dmmulpq  7528  archnqq  7565  prarloclemarch2  7567  prarloclemlt  7641  cnegex  8285  nnge1  9094  zneo  9509  fsum2d  11861  fsumabs  11891  fsumiun  11903  fprod2d  12049  efne0  12104  nn0o1gt2  12331  ennnfonelemex  12900  qtopbasss  15108  ivthdichlem  15238  dvmptfsum  15312  reeff1o  15360  coseq0negpitopi  15423  cos02pilt1  15438  logltb  15461  gausslemma2dlem0i  15649  2lgs  15696  bdop  16010  bj-nntrans  16086