Theorem mpancom

Description: An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003) (Proof shortened by Wolf Lammen, 7-Apr-2013)

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

Proof

Step	Hyp	Ref	Expression
1		mpancom.1	$$⊢\psi \to \phi$$
2		mpancom.2	$$⊢\left(\phi \wedge \psi \right)\to \chi$$
3		id	$$⊢\psi \to \psi$$
4	1 3 2	syl2anc	$$⊢\psi \to \chi$$