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  623  simplimdc  860  mp3an3  1326  3impexpbicom  1438  mpisyl  1446  equcomi  1704  equsex  1728  equsexd  1729  spimt  1736  spimeh  1739  equvini  1758  equveli  1759  sbcof2  1810  dveeq2  1815  ax11v2  1820  ax16i  1858  pm13.183  2877  euxfr2dc  2924  sbcth  2978  sbcth2  3052  ssun3  3302  ssun4  3303  ralf0  3528  exmidexmid  4198  rext  4217  exss  4229  uniopel  4258  onsucelsucexmid  4531  suc11g  4558  eunex  4562  ordsoexmid  4563  tfisi  4588  finds1  4603  omsinds  4623  relop  4779  dmrnssfld  4892  iss  4955  relcoi1  5162  nfunv  5251  funimass2  5296  fvssunirng  5532  fvmptg  5594  oprabidlem  5908  fovcl  5982  elovmpo  6074  tfrlem1  6311  oaword1  6474  0domg  6839  diffifi  6896  exmidpw  6910  djulclb  7056  0ct  7108  nlt1pig  7342  dmaddpq  7380  dmmulpq  7381  archnqq  7418  prarloclemarch2  7420  prarloclemlt  7494  cnegex  8137  nnge1  8944  zneo  9356  fsum2d  11445  fsumabs  11475  fsumiun  11487  fprod2d  11633  efne0  11688  nn0o1gt2  11912  ennnfonelemex  12417  qtopbasss  14106  reeff1o  14279  coseq0negpitopi  14342  cos02pilt1  14357  logltb  14380  bdop  14712  bj-nntrans  14788