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  628  simplimdc  867  mp3an3  1362  3impexpbicom  1483  mpisyl  1491  equcomi  1752  equsex  1776  equsexd  1777  spimt  1784  spimeh  1787  equvini  1806  equveli  1807  sbcof2  1858  dveeq2  1863  ax11v2  1868  ax16i  1906  pm13.183  2944  euxfr2dc  2991  sbcth  3045  sbcth2  3120  ssun3  3372  ssun4  3373  ralf0  3597  exmidexmid  4286  rext  4307  exss  4319  uniopel  4349  onsucelsucexmid  4628  suc11g  4655  eunex  4659  ordsoexmid  4660  tfisi  4685  finds1  4700  omsinds  4720  relop  4880  dmrnssfld  4995  iss  5059  relcoi1  5268  nfunv  5359  funimass2  5408  fvssunirng  5654  fvmptg  5722  oprabidlem  6049  elovmpo  6221  tfrlem1  6474  oaword1  6639  modom  6994  0domg  7023  1ndom2  7051  diffifi  7083  exmidpw  7100  djulclb  7254  0ct  7306  iftrueb01  7441  nlt1pig  7561  dmaddpq  7599  dmmulpq  7600  archnqq  7637  prarloclemarch2  7639  prarloclemlt  7713  cnegex  8357  nnge1  9166  zneo  9581  fsum2d  12001  fsumabs  12031  fsumiun  12043  fprod2d  12189  efne0  12244  nn0o1gt2  12471  ennnfonelemex  13040  qtopbasss  15251  ivthdichlem  15381  dvmptfsum  15455  reeff1o  15503  coseq0negpitopi  15566  cos02pilt1  15581  logltb  15604  gausslemma2dlem0i  15792  2lgs  15839  bdop  16496  bj-nntrans  16572