Theorem mp2an

Description: An inference based on modus ponens. (Contributed by NM, 13-Apr-1995)

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

Proof

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