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  862  mp3an3  1339  3impexpbicom  1458  mpisyl  1466  equcomi  1727  equsex  1751  equsexd  1752  spimt  1759  spimeh  1762  equvini  1781  equveli  1782  sbcof2  1833  dveeq2  1838  ax11v2  1843  ax16i  1881  pm13.183  2911  euxfr2dc  2958  sbcth  3012  sbcth2  3086  ssun3  3338  ssun4  3339  ralf0  3563  exmidexmid  4240  rext  4259  exss  4271  uniopel  4301  onsucelsucexmid  4578  suc11g  4605  eunex  4609  ordsoexmid  4610  tfisi  4635  finds1  4650  omsinds  4670  relop  4828  dmrnssfld  4941  iss  5005  relcoi1  5214  nfunv  5304  funimass2  5352  fvssunirng  5591  fvmptg  5655  oprabidlem  5975  elovmpo  6145  tfrlem1  6394  oaword1  6557  0domg  6934  diffifi  6991  exmidpw  7005  djulclb  7157  0ct  7209  nlt1pig  7454  dmaddpq  7492  dmmulpq  7493  archnqq  7530  prarloclemarch2  7532  prarloclemlt  7606  cnegex  8250  nnge1  9059  zneo  9474  fsum2d  11746  fsumabs  11776  fsumiun  11788  fprod2d  11934  efne0  11989  nn0o1gt2  12216  ennnfonelemex  12785  qtopbasss  14993  ivthdichlem  15123  dvmptfsum  15197  reeff1o  15245  coseq0negpitopi  15308  cos02pilt1  15323  logltb  15346  gausslemma2dlem0i  15534  2lgs  15581  bdop  15811  bj-nntrans  15887