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  626  simplimdc  865  mp3an3  1360  3impexpbicom  1481  mpisyl  1489  equcomi  1750  equsex  1774  equsexd  1775  spimt  1782  spimeh  1785  equvini  1804  equveli  1805  sbcof2  1856  dveeq2  1861  ax11v2  1866  ax16i  1904  pm13.183  2941  euxfr2dc  2988  sbcth  3042  sbcth2  3117  ssun3  3369  ssun4  3370  ralf0  3594  exmidexmid  4279  rext  4300  exss  4312  uniopel  4342  onsucelsucexmid  4621  suc11g  4648  eunex  4652  ordsoexmid  4653  tfisi  4678  finds1  4693  omsinds  4713  relop  4871  dmrnssfld  4986  iss  5050  relcoi1  5259  nfunv  5350  funimass2  5398  fvssunirng  5641  fvmptg  5709  oprabidlem  6031  elovmpo  6203  tfrlem1  6452  oaword1  6615  0domg  6994  1ndom2  7022  diffifi  7052  exmidpw  7066  djulclb  7218  0ct  7270  iftrueb01  7404  nlt1pig  7524  dmaddpq  7562  dmmulpq  7563  archnqq  7600  prarloclemarch2  7602  prarloclemlt  7676  cnegex  8320  nnge1  9129  zneo  9544  fsum2d  11941  fsumabs  11971  fsumiun  11983  fprod2d  12129  efne0  12184  nn0o1gt2  12411  ennnfonelemex  12980  qtopbasss  15189  ivthdichlem  15319  dvmptfsum  15393  reeff1o  15441  coseq0negpitopi  15504  cos02pilt1  15519  logltb  15542  gausslemma2dlem0i  15730  2lgs  15777  bdop  16196  bj-nntrans  16272