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  6584  oaword1  6749  modom  7114  0domg  7143  1ndom2  7172  diffifi  7204  exmidpw  7221  djulclb  7401  0ct  7453  iftrueb01  7588  nlt1pig  7714  dmaddpq  7752  dmmulpq  7753  archnqq  7790  prarloclemarch2  7792  prarloclemlt  7866  cnegex  8511  nnge1  9336  zneo  9757  resq01  11115  fsum2d  12226  fsumabs  12256  fsumiun  12268  fprod2d  12414  efne0  12469  nn0o1gt2  12696  ennnfonelemex  13362  qtopbasss  15764  ivthdichlem  15894  dvmptfsum  15968  reeff1o  16016  coseq0negpitopi  16080  cos02pilt1  16096  logltb  16121  pellexlem3  16248  gausslemma2dlem0i  16398  2lgs  16445  bdop  17123  bj-nntrans  17199  exmidcon  17259