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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mp2  16  syl6mpi  64  mp2ani  436  pm2.24i  632  simplimdc  872  mp3an3  1367  3impexpbicom  1488  mpisyl  1496  equcomi  1756  equsex  1780  equsexd  1782  spimt  1789  spimeh  1792  equvini  1811  equveli  1812  sbcof2  1863  dveeq2  1868  ax11v2  1873  ax16i  1911  pm13.183  2964  euxfr2dc  3011  sbcth  3065  sbcth2  3140  ssun3  3394  ssun4  3395  ralf0  3630  exmidexmid  4333  rext  4355  exss  4367  uniopel  4397  onsucelsucexmid  4677  suc11g  4704  eunex  4708  ordsoexmid  4709  tfisi  4734  finds1  4749  omsinds  4769  relop  4930  dmrnssfld  5045  iss  5109  relcoi1  5319  nfunv  5410  funimass2  5459  fvssunirng  5710  fvmptg  5781  oprabidlem  6116  elovmpo  6288  tfrlem1  6579  oaword1  6744  modom  7108  0domg  7137  1ndom2  7166  diffifi  7198  exmidpw  7215  djulclb  7395  0ct  7447  iftrueb01  7582  nlt1pig  7708  dmaddpq  7746  dmmulpq  7747  archnqq  7784  prarloclemarch2  7786  prarloclemlt  7860  cnegex  8504  nnge1  9327  zneo  9747  resq01  11095  fsum2d  12202  fsumabs  12232  fsumiun  12244  fprod2d  12390  efne0  12445  nn0o1gt2  12672  ennnfonelemex  13305  qtopbasss  15622  ivthdichlem  15752  dvmptfsum  15826  reeff1o  15874  coseq0negpitopi  15937  cos02pilt1  15952  logltb  15975  pellexlem3  16093  gausslemma2dlem0i  16176  2lgs  16223  bdop  16901  bj-nntrans  16977  exmidcon  17037