Theorem mpi 16

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 10	. 2 ⊢ (φ → ψ)
3		mpi.2	. 2 ⊢ (φ → (ψ → χ))
4	2, 3	mpd 14	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  17  syl6mpi  58  mp2ani  659  mp3an3  1266  3impexpbicom  1367  ee10  1376  merco2  1501  equcomi  1679  ax10  1944  equveli  1988  ax11v2  1992  ax11eq  2193  ax11el  2194  ax11inda  2200  ax11v2-o  2201  pm13.183  2980  sbcth  3061  sbcth2  3130  ssun3  3429  ssun4  3430  uneqdifeq  3639  ralf0  3657  uniintsn  3964  opkth1g  4131  funimass2  5171  fvopab4g  5389  fovcl  5589  ov2ag  5599  ov3  5600  fnfreclem3  6320