Theorem mp2an

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

	Ref	Expression
Hypotheses	mp2an.1	$$⊢\phi$$
	mp2an.2	$$⊢\psi$$
	mp2an.3	$$⊢\left(\phi \wedge \psi \right)\to \chi$$
Assertion	mp2an	$$⊢\chi$$

Proof

Step	Hyp	Ref	Expression
1		mp2an.1	$$⊢\phi$$
2		mp2an.2	$$⊢\psi$$
3		mp2an.3	$$⊢\left(\phi \wedge \psi \right)\to \chi$$
4	1 3	mpan	$$⊢\psi \to \chi$$
5	2 4	ax-mp	$$⊢\chi$$