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  626  simplimdc  865  mp3an3  1360  3impexpbicom  1481  mpisyl  1489  equcomi  1750  equsex  1774  equsexd  1775  spimt  1782  spimeh  1785  equvini  1804  equveli  1805  sbcof2  1856  dveeq2  1861  ax11v2  1866  ax16i  1904  pm13.183  2941  euxfr2dc  2988  sbcth  3042  sbcth2  3117  ssun3  3369  ssun4  3370  ralf0  3594  exmidexmid  4280  rext  4301  exss  4313  uniopel  4343  onsucelsucexmid  4622  suc11g  4649  eunex  4653  ordsoexmid  4654  tfisi  4679  finds1  4694  omsinds  4714  relop  4872  dmrnssfld  4987  iss  5051  relcoi1  5260  nfunv  5351  funimass2  5399  fvssunirng  5642  fvmptg  5710  oprabidlem  6032  elovmpo  6204  tfrlem1  6454  oaword1  6617  0domg  6998  1ndom2  7026  diffifi  7056  exmidpw  7070  djulclb  7222  0ct  7274  iftrueb01  7408  nlt1pig  7528  dmaddpq  7566  dmmulpq  7567  archnqq  7604  prarloclemarch2  7606  prarloclemlt  7680  cnegex  8324  nnge1  9133  zneo  9548  fsum2d  11946  fsumabs  11976  fsumiun  11988  fprod2d  12134  efne0  12189  nn0o1gt2  12416  ennnfonelemex  12985  qtopbasss  15195  ivthdichlem  15325  dvmptfsum  15399  reeff1o  15447  coseq0negpitopi  15510  cos02pilt1  15525  logltb  15548  gausslemma2dlem0i  15736  2lgs  15783  bdop  16238  bj-nntrans  16314