Theorem mp2b

Description: A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013)

	Ref	Expression
Hypotheses	mp2b.1	$$⊢\phi$$
	mp2b.2	$$⊢\phi \to \psi$$
	mp2b.3	$$⊢\psi \to \chi$$
Assertion	mp2b	$$⊢\chi$$

Proof

Step	Hyp	Ref	Expression
1		mp2b.1	$$⊢\phi$$
2		mp2b.2	$$⊢\phi \to \psi$$
3		mp2b.3	$$⊢\psi \to \chi$$
4	1 2	ax-mp	$$⊢\psi$$
5	4 3	ax-mp	$$⊢\chi$$