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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  mp2  16  syl6mpi  62  mp2ani  416  pm2.24i  563  simplimdc  768  mp3an3  1232  3impexpbicom  1343  mpisyl  1351  equcomi  1608  equsex  1632  equsexd  1633  spimt  1640  spimeh  1643  equvini  1657  equveli  1658  sbcof2  1707  dveeq2  1712  ax11v2  1717  ax16i  1754  pm13.183  2703  euxfr2dc  2748  sbcth  2799  sbcth2  2872  ssun3  3135  ssun4  3136  ralf0  3351  rext  3978  exss  3990  uniopel  4020  onsucelsucexmid  4282  suc11g  4308  eunex  4312  ordsoexmid  4313  tfisi  4337  finds1  4352  relop  4513  dmrnssfld  4622  iss  4681  relcoi1  4876  nfunv  4960  funimass2  5004  fvssunirng  5217  fvmptg  5275  oprabidlem  5563  fovcl  5633  elovmpt2  5728  tfrlem1  5953  oaword1  6080  diffifi  6381  nlt1pig  6496  dmaddpq  6534  dmmulpq  6535  archnqq  6572  prarloclemarch2  6574  prarloclemlt  6648  cnegex  7251  nnge1  8012  zneo  8397  nn0o1gt2  10209  bdop  10354  bj-nntrans  10435