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	⊢ ( 𝜓 → 𝜑 )
	mpancom.2	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
Assertion	mpancom	⊢ ( 𝜓 → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		mpancom.1	⊢ ( 𝜓 → 𝜑 )
2		mpancom.2	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
3		id	⊢ ( 𝜓 → 𝜓 )
4	1 3 2	syl2anc	⊢ ( 𝜓 → 𝜒 )