Theorem mpi

Description: A nested modus ponens inference. Inference associated with com12 . (Contributed by NM, 29-Dec-1992) (Proof shortened by Stefan Allan, 20-Mar-2006)

	Ref	Expression
Hypotheses	mpi.1	⊢ 𝜓
	mpi.2	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
Assertion	mpi	⊢ ( 𝜑 → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		mpi.1	⊢ 𝜓
2		mpi.2	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
3	1	a1i	⊢ ( 𝜑 → 𝜓 )
4	3 2	mpd	⊢ ( 𝜑 → 𝜒 )