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  428  pm2.24i  612  simplimdc  845  mp3an3  1304  3impexpbicom  1414  mpisyl  1422  equcomi  1680  equsex  1706  equsexd  1707  spimt  1714  spimeh  1717  equvini  1731  equveli  1732  sbcof2  1782  dveeq2  1787  ax11v2  1792  ax16i  1830  pm13.183  2817  euxfr2dc  2864  sbcth  2917  sbcth2  2991  ssun3  3236  ssun4  3237  ralf0  3461  exmidexmid  4115  rext  4132  exss  4144  uniopel  4173  onsucelsucexmid  4440  suc11g  4467  eunex  4471  ordsoexmid  4472  tfisi  4496  finds1  4511  omsinds  4530  relop  4684  dmrnssfld  4797  iss  4860  relcoi1  5065  nfunv  5151  funimass2  5196  fvssunirng  5429  fvmptg  5490  oprabidlem  5795  fovcl  5869  elovmpo  5964  tfrlem1  6198  oaword1  6360  0domg  6724  diffifi  6781  exmidpw  6795  djulclb  6933  0ct  6985  nlt1pig  7142  dmaddpq  7180  dmmulpq  7181  archnqq  7218  prarloclemarch2  7220  prarloclemlt  7294  cnegex  7933  nnge1  8736  zneo  9145  fsum2d  11197  fsumabs  11227  fsumiun  11239  efne0  11373  nn0o1gt2  11591  ennnfonelemex  11916  qtopbasss  12679  coseq0negpitopi  12906  cos02pilt1  12921  bdop  13062  bj-nntrans  13138