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 )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mp2  16  syl6mpi  64  mp2ani  436  pm2.24i  632  simplimdc  872  mp3an3  1367  3impexpbicom  1488  mpisyl  1496  equcomi  1756  equsex  1780  equsexd  1782  spimt  1789  spimeh  1792  equvini  1811  equveli  1812  sbcof2  1863  dveeq2  1868  ax11v2  1873  ax16i  1911  pm13.183  2964  euxfr2dc  3011  sbcth  3065  sbcth2  3140  ssun3  3394  ssun4  3395  ralf0  3630  exmidexmid  4335  rext  4357  exss  4369  uniopel  4399  onsucelsucexmid  4679  suc11g  4706  eunex  4710  ordsoexmid  4711  tfisi  4736  finds1  4751  omsinds  4771  relop  4932  dmrnssfld  5047  iss  5112  relcoi1  5322  nfunv  5413  funimass2  5462  fvssunirng  5713  fvmptg  5784  oprabidlem  6119  elovmpo  6291  tfrlem1  6583  oaword1  6748  modom  7112  0domg  7141  1ndom2  7170  diffifi  7202  exmidpw  7219  djulclb  7401  0ct  7453  iftrueb01  7588  nlt1pig  7714  dmaddpq  7752  dmmulpq  7753  archnqq  7790  prarloclemarch2  7792  prarloclemlt  7866  cnegex  8511  nnge1  9336  zneo  9758  resq01  11116  fsum2d  12227  fsumabs  12257  fsumiun  12269  fprod2d  12415  efne0  12470  nn0o1gt2  12697  ennnfonelemex  13363  qtopbasss  15747  ivthdichlem  15877  dvmptfsum  15951  reeff1o  15999  coseq0negpitopi  16063  cos02pilt1  16079  logltb  16104  pellexlem3  16231  gausslemma2dlem0i  16381  2lgs  16428  bdop  17106  bj-nntrans  17182  exmidcon  17242