Theorem mp2

Description: A double modus ponens inference. (Contributed by NM, 5-Apr-1994)

	Ref	Expression
Hypotheses	mp2.1	$$⊢\phi$$
	mp2.2	$$⊢\psi$$
	mp2.3	$$⊢\phi \to \left(\psi \to \chi \right)$$
Assertion	mp2	$$⊢\chi$$

Proof

Step	Hyp	Ref	Expression
1		mp2.1	$$⊢\phi$$
2		mp2.2	$$⊢\psi$$
3		mp2.3	$$⊢\phi \to \left(\psi \to \chi \right)$$
4	1 3	ax-mp	$$⊢\psi \to \chi$$
5	2 4	ax-mp	$$⊢\chi$$