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  868  mp3an3  1363  3impexpbicom  1484  mpisyl  1492  equcomi  1752  equsex  1776  equsexd  1778  spimt  1785  spimeh  1788  equvini  1807  equveli  1808  sbcof2  1859  dveeq2  1864  ax11v2  1869  ax16i  1907  pm13.183  2958  euxfr2dc  3005  sbcth  3059  sbcth2  3134  ssun3  3388  ssun4  3389  ralf0  3616  exmidexmid  4314  rext  4336  exss  4348  uniopel  4378  onsucelsucexmid  4657  suc11g  4684  eunex  4688  ordsoexmid  4689  tfisi  4714  finds1  4729  omsinds  4749  relop  4910  dmrnssfld  5025  iss  5089  relcoi1  5299  nfunv  5390  funimass2  5439  fvssunirng  5690  fvmptg  5758  oprabidlem  6089  elovmpo  6261  tfrlem1  6552  oaword1  6717  modom  7074  0domg  7103  1ndom2  7132  diffifi  7164  exmidpw  7181  djulclb  7359  0ct  7411  iftrueb01  7546  nlt1pig  7672  dmaddpq  7710  dmmulpq  7711  archnqq  7748  prarloclemarch2  7750  prarloclemlt  7824  cnegex  8467  nnge1  9277  zneo  9697  resq01  11044  fsum2d  12146  fsumabs  12176  fsumiun  12188  fprod2d  12334  efne0  12389  nn0o1gt2  12616  ennnfonelemex  13249  qtopbasss  15512  ivthdichlem  15642  dvmptfsum  15716  reeff1o  15764  coseq0negpitopi  15827  cos02pilt1  15842  logltb  15865  pellexlem3  15973  gausslemma2dlem0i  16056  2lgs  16103  bdop  16771  bj-nntrans  16847  exmidcon  16906