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  3328  ssun4  3329  ralf0  3553  exmidexmid  4229  rext  4248  exss  4260  uniopel  4289  onsucelsucexmid  4566  suc11g  4593  eunex  4597  ordsoexmid  4598  tfisi  4623  finds1  4638  omsinds  4658  relop  4816  dmrnssfld  4929  iss  4992  relcoi1  5201  nfunv  5291  funimass2  5336  fvssunirng  5573  fvmptg  5637  oprabidlem  5953  elovmpo  6122  tfrlem1  6366  oaword1  6529  0domg  6898  diffifi  6955  exmidpw  6969  djulclb  7121  0ct  7173  nlt1pig  7408  dmaddpq  7446  dmmulpq  7447  archnqq  7484  prarloclemarch2  7486  prarloclemlt  7560  cnegex  8204  nnge1  9013  zneo  9427  fsum2d  11600  fsumabs  11630  fsumiun  11642  fprod2d  11788  efne0  11843  nn0o1gt2  12070  ennnfonelemex  12631  qtopbasss  14757  ivthdichlem  14887  dvmptfsum  14961  reeff1o  15009  coseq0negpitopi  15072  cos02pilt1  15087  logltb  15110  gausslemma2dlem0i  15298  2lgs  15345  bdop  15521  bj-nntrans  15597