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  7425  dmaddpq  7463  dmmulpq  7464  archnqq  7501  prarloclemarch2  7503  prarloclemlt  7577  cnegex  8221  nnge1  9030  zneo  9444  fsum2d  11617  fsumabs  11647  fsumiun  11659  fprod2d  11805  efne0  11860  nn0o1gt2  12087  ennnfonelemex  12656  qtopbasss  14841  ivthdichlem  14971  dvmptfsum  15045  reeff1o  15093  coseq0negpitopi  15156  cos02pilt1  15171  logltb  15194  gausslemma2dlem0i  15382  2lgs  15429  bdop  15605  bj-nntrans  15681