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  861  mp3an3  1337  3impexpbicom  1449  mpisyl  1457  equcomi  1715  equsex  1739  equsexd  1740  spimt  1747  spimeh  1750  equvini  1769  equveli  1770  sbcof2  1821  dveeq2  1826  ax11v2  1831  ax16i  1869  pm13.183  2890  euxfr2dc  2937  sbcth  2991  sbcth2  3065  ssun3  3315  ssun4  3316  ralf0  3541  exmidexmid  4214  rext  4233  exss  4245  uniopel  4274  onsucelsucexmid  4547  suc11g  4574  eunex  4578  ordsoexmid  4579  tfisi  4604  finds1  4619  omsinds  4639  relop  4795  dmrnssfld  4908  iss  4971  relcoi1  5178  nfunv  5268  funimass2  5313  fvssunirng  5549  fvmptg  5613  oprabidlem  5928  elovmpo  6096  tfrlem1  6334  oaword1  6497  0domg  6866  diffifi  6923  exmidpw  6937  djulclb  7085  0ct  7137  nlt1pig  7371  dmaddpq  7409  dmmulpq  7410  archnqq  7447  prarloclemarch2  7449  prarloclemlt  7523  cnegex  8166  nnge1  8973  zneo  9385  fsum2d  11478  fsumabs  11508  fsumiun  11520  fprod2d  11666  efne0  11721  nn0o1gt2  11945  ennnfonelemex  12468  qtopbasss  14498  reeff1o  14671  coseq0negpitopi  14734  cos02pilt1  14749  logltb  14772  bdop  15105  bj-nntrans  15181