Theorem mp2b

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

	Ref	Expression
Hypotheses	mp2b.1	|- ph
	mp2b.2	|- ( ph -> ps )
	mp2b.3	|- ( ps -> ch )
Assertion	mp2b	|- ch

Proof

Step	Hyp	Ref	Expression
1		mp2b.1	|- ph
2		mp2b.2	|- ( ph -> ps )
3		mp2b.3	|- ( ps -> ch )
4	1 2	ax-mp	|- ps
5	4 3	ax-mp	|- ch