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  628  simplimdc  867  mp3an3  1362  3impexpbicom  1483  mpisyl  1491  equcomi  1752  equsex  1776  equsexd  1777  spimt  1784  spimeh  1787  equvini  1806  equveli  1807  sbcof2  1858  dveeq2  1863  ax11v2  1868  ax16i  1906  pm13.183  2944  euxfr2dc  2991  sbcth  3045  sbcth2  3120  ssun3  3372  ssun4  3373  ralf0  3597  exmidexmid  4286  rext  4307  exss  4319  uniopel  4349  onsucelsucexmid  4628  suc11g  4655  eunex  4659  ordsoexmid  4660  tfisi  4685  finds1  4700  omsinds  4720  relop  4880  dmrnssfld  4995  iss  5059  relcoi1  5268  nfunv  5359  funimass2  5408  fvssunirng  5654  fvmptg  5722  oprabidlem  6048  elovmpo  6220  tfrlem1  6473  oaword1  6638  modom  6993  0domg  7022  1ndom2  7050  diffifi  7082  exmidpw  7099  djulclb  7253  0ct  7305  iftrueb01  7440  nlt1pig  7560  dmaddpq  7598  dmmulpq  7599  archnqq  7636  prarloclemarch2  7638  prarloclemlt  7712  cnegex  8356  nnge1  9165  zneo  9580  fsum2d  11995  fsumabs  12025  fsumiun  12037  fprod2d  12183  efne0  12238  nn0o1gt2  12465  ennnfonelemex  13034  qtopbasss  15244  ivthdichlem  15374  dvmptfsum  15448  reeff1o  15496  coseq0negpitopi  15559  cos02pilt1  15574  logltb  15597  gausslemma2dlem0i  15785  2lgs  15832  bdop  16470  bj-nntrans  16546