Theorem mp2b

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

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

Proof

Step	Hyp	Ref	Expression
1		mp2b.1	⊢ 𝜑
2		mp2b.2	⊢ ( 𝜑 → 𝜓 )
3		mp2b.3	⊢ ( 𝜓 → 𝜒 )
4	1 2	ax-mp	⊢ 𝜓
5	4 3	ax-mp	⊢ 𝜒