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  4280  rext  4301  exss  4313  uniopel  4343  onsucelsucexmid  4622  suc11g  4649  eunex  4653  ordsoexmid  4654  tfisi  4679  finds1  4694  omsinds  4714  relop  4872  dmrnssfld  4987  iss  5051  relcoi1  5260  nfunv  5351  funimass2  5399  fvssunirng  5644  fvmptg  5712  oprabidlem  6038  elovmpo  6210  tfrlem1  6460  oaword1  6625  0domg  7006  1ndom2  7034  diffifi  7064  exmidpw  7081  djulclb  7233  0ct  7285  iftrueb01  7419  nlt1pig  7539  dmaddpq  7577  dmmulpq  7578  archnqq  7615  prarloclemarch2  7617  prarloclemlt  7691  cnegex  8335  nnge1  9144  zneo  9559  fsum2d  11961  fsumabs  11991  fsumiun  12003  fprod2d  12149  efne0  12204  nn0o1gt2  12431  ennnfonelemex  13000  qtopbasss  15210  ivthdichlem  15340  dvmptfsum  15414  reeff1o  15462  coseq0negpitopi  15525  cos02pilt1  15540  logltb  15563  gausslemma2dlem0i  15751  2lgs  15798  bdop  16293  bj-nntrans  16369