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	|- ( ps -> ph )
	mpancom.2	|- ( ( ph /\ ps ) -> ch )
Assertion	mpancom	|- ( ps -> ch )

Proof

Step	Hyp	Ref	Expression
1		mpancom.1	|- ( ps -> ph )
2		mpancom.2	|- ( ( ph /\ ps ) -> ch )
3		id	|- ( ps -> ps )
4	1 3 2	syl2anc	|- ( ps -> ch )