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	⊢ 𝜓
mpi.2	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
mpi	⊢ (𝜑 → 𝜒)

Proof of Theorem mpi

Step	Hyp	Ref	Expression
1		mpi.1	. . 3 ⊢ 𝜓
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝜓)
3		mpi.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	mpd 13	1 ⊢ (𝜑 → 𝜒)

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  1718  equsex  1742  equsexd  1743  spimt  1750  spimeh  1753  equvini  1772  equveli  1773  sbcof2  1824  dveeq2  1829  ax11v2  1834  ax16i  1872  pm13.183  2902  euxfr2dc  2949  sbcth  3003  sbcth2  3077  ssun3  3329  ssun4  3330  ralf0  3554  exmidexmid  4230  rext  4249  exss  4261  uniopel  4290  onsucelsucexmid  4567  suc11g  4594  eunex  4598  ordsoexmid  4599  tfisi  4624  finds1  4639  omsinds  4659  relop  4817  dmrnssfld  4930  iss  4993  relcoi1  5202  nfunv  5292  funimass2  5337  fvssunirng  5576  fvmptg  5640  oprabidlem  5956  elovmpo  6126  tfrlem1  6375  oaword1  6538  0domg  6907  diffifi  6964  exmidpw  6978  djulclb  7130  0ct  7182  nlt1pig  7427  dmaddpq  7465  dmmulpq  7466  archnqq  7503  prarloclemarch2  7505  prarloclemlt  7579  cnegex  8223  nnge1  9032  zneo  9446  fsum2d  11619  fsumabs  11649  fsumiun  11661  fprod2d  11807  efne0  11862  nn0o1gt2  12089  ennnfonelemex  12658  qtopbasss  14843  ivthdichlem  14973  dvmptfsum  15047  reeff1o  15095  coseq0negpitopi  15158  cos02pilt1  15173  logltb  15196  gausslemma2dlem0i  15384  2lgs  15431  bdop  15607  bj-nntrans  15683