Theorem mp2

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

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

Proof

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