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  428  pm2.24i  612  simplimdc  845  mp3an3  1304  3impexpbicom  1414  mpisyl  1422  equcomi  1680  equsex  1706  equsexd  1707  spimt  1714  spimeh  1717  equvini  1731  equveli  1732  sbcof2  1782  dveeq2  1787  ax11v2  1792  ax16i  1830  pm13.183  2822  euxfr2dc  2869  sbcth  2922  sbcth2  2996  ssun3  3241  ssun4  3242  ralf0  3466  exmidexmid  4120  rext  4137  exss  4149  uniopel  4178  onsucelsucexmid  4445  suc11g  4472  eunex  4476  ordsoexmid  4477  tfisi  4501  finds1  4516  omsinds  4535  relop  4689  dmrnssfld  4802  iss  4865  relcoi1  5070  nfunv  5156  funimass2  5201  fvssunirng  5436  fvmptg  5497  oprabidlem  5802  fovcl  5876  elovmpo  5971  tfrlem1  6205  oaword1  6367  0domg  6731  diffifi  6788  exmidpw  6802  djulclb  6940  0ct  6992  nlt1pig  7149  dmaddpq  7187  dmmulpq  7188  archnqq  7225  prarloclemarch2  7227  prarloclemlt  7301  cnegex  7940  nnge1  8743  zneo  9152  fsum2d  11204  fsumabs  11234  fsumiun  11246  efne0  11384  nn0o1gt2  11602  ennnfonelemex  11927  qtopbasss  12690  coseq0negpitopi  12917  cos02pilt1  12932  bdop  13073  bj-nntrans  13149