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  623  simplimdc  860  mp3an3  1326  3impexpbicom  1436  mpisyl  1444  equcomi  1702  equsex  1726  equsexd  1727  spimt  1734  spimeh  1737  equvini  1756  equveli  1757  sbcof2  1808  dveeq2  1813  ax11v2  1818  ax16i  1856  pm13.183  2873  euxfr2dc  2920  sbcth  2974  sbcth2  3048  ssun3  3298  ssun4  3299  ralf0  3524  exmidexmid  4191  rext  4209  exss  4221  uniopel  4250  onsucelsucexmid  4523  suc11g  4550  eunex  4554  ordsoexmid  4555  tfisi  4580  finds1  4595  omsinds  4615  relop  4770  dmrnssfld  4883  iss  4946  relcoi1  5152  nfunv  5241  funimass2  5286  fvssunirng  5522  fvmptg  5584  oprabidlem  5896  fovcl  5970  elovmpo  6062  tfrlem1  6299  oaword1  6462  0domg  6827  diffifi  6884  exmidpw  6898  djulclb  7044  0ct  7096  nlt1pig  7315  dmaddpq  7353  dmmulpq  7354  archnqq  7391  prarloclemarch2  7393  prarloclemlt  7467  cnegex  8109  nnge1  8913  zneo  9325  fsum2d  11409  fsumabs  11439  fsumiun  11451  fprod2d  11597  efne0  11652  nn0o1gt2  11875  ennnfonelemex  12380  qtopbasss  13572  reeff1o  13745  coseq0negpitopi  13808  cos02pilt1  13823  logltb  13846  bdop  14167  bj-nntrans  14243