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	$$⊢\psi$$
	mpi.2	$$⊢\phi \to \left(\psi \to \chi \right)$$
Assertion	mpi	$$⊢\phi \to \chi$$

Proof

Step	Hyp	Ref	Expression
1		mpi.1	$$⊢\psi$$
2		mpi.2	$$⊢\phi \to \left(\psi \to \chi \right)$$
3	1	a1i	$$⊢\phi \to \psi$$
4	3 2	mpd	$$⊢\phi \to \chi$$