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  429  pm2.24i  613  simplimdc  846  mp3an3  1305  3impexpbicom  1415  mpisyl  1423  equcomi  1681  equsex  1707  equsexd  1708  spimt  1715  spimeh  1718  equvini  1732  equveli  1733  sbcof2  1783  dveeq2  1788  ax11v2  1793  ax16i  1831  pm13.183  2826  euxfr2dc  2873  sbcth  2926  sbcth2  3000  ssun3  3246  ssun4  3247  ralf0  3471  exmidexmid  4128  rext  4145  exss  4157  uniopel  4186  onsucelsucexmid  4453  suc11g  4480  eunex  4484  ordsoexmid  4485  tfisi  4509  finds1  4524  omsinds  4543  relop  4697  dmrnssfld  4810  iss  4873  relcoi1  5078  nfunv  5164  funimass2  5209  fvssunirng  5444  fvmptg  5505  oprabidlem  5810  fovcl  5884  elovmpo  5979  tfrlem1  6213  oaword1  6375  0domg  6739  diffifi  6796  exmidpw  6810  djulclb  6948  0ct  7000  nlt1pig  7173  dmaddpq  7211  dmmulpq  7212  archnqq  7249  prarloclemarch2  7251  prarloclemlt  7325  cnegex  7964  nnge1  8767  zneo  9176  fsum2d  11236  fsumabs  11266  fsumiun  11278  efne0  11421  nn0o1gt2  11638  ennnfonelemex  11963  qtopbasss  12729  reeff1o  12902  coseq0negpitopi  12965  cos02pilt1  12980  logltb  13003  bdop  13244  bj-nntrans  13320