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  7396  0ct  7448  iftrueb01  7583  nlt1pig  7709  dmaddpq  7747  dmmulpq  7748  archnqq  7785  prarloclemarch2  7787  prarloclemlt  7861  cnegex  8506  nnge1  9330  zneo  9752  resq01  11110  fsum2d  12221  fsumabs  12251  fsumiun  12263  fprod2d  12409  efne0  12464  nn0o1gt2  12691  ennnfonelemex  13357  qtopbasss  15713  ivthdichlem  15843  dvmptfsum  15917  reeff1o  15965  coseq0negpitopi  16029  cos02pilt1  16044  logltb  16068  pellexlem3  16192  gausslemma2dlem0i  16342  2lgs  16389  bdop  17067  bj-nntrans  17143  exmidcon  17203