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  868  mp3an3  1363  3impexpbicom  1484  mpisyl  1492  equcomi  1752  equsex  1776  equsexd  1777  spimt  1784  spimeh  1787  equvini  1806  equveli  1807  sbcof2  1858  dveeq2  1863  ax11v2  1868  ax16i  1906  pm13.183  2945  euxfr2dc  2992  sbcth  3046  sbcth2  3121  ssun3  3374  ssun4  3375  ralf0  3599  exmidexmid  4292  rext  4313  exss  4325  uniopel  4355  onsucelsucexmid  4634  suc11g  4661  eunex  4665  ordsoexmid  4666  tfisi  4691  finds1  4706  omsinds  4726  relop  4886  dmrnssfld  5001  iss  5065  relcoi1  5275  nfunv  5366  funimass2  5415  fvssunirng  5663  fvmptg  5731  oprabidlem  6059  elovmpo  6231  tfrlem1  6517  oaword1  6682  modom  7037  0domg  7066  1ndom2  7094  diffifi  7126  exmidpw  7143  djulclb  7297  0ct  7349  iftrueb01  7484  nlt1pig  7604  dmaddpq  7642  dmmulpq  7643  archnqq  7680  prarloclemarch2  7682  prarloclemlt  7756  cnegex  8399  nnge1  9208  zneo  9625  fsum2d  12059  fsumabs  12089  fsumiun  12101  fprod2d  12247  efne0  12302  nn0o1gt2  12529  ennnfonelemex  13098  qtopbasss  15315  ivthdichlem  15445  dvmptfsum  15519  reeff1o  15567  coseq0negpitopi  15630  cos02pilt1  15645  logltb  15668  pellexlem3  15776  gausslemma2dlem0i  15859  2lgs  15906  bdop  16574  bj-nntrans  16650  exmidcon  16711