Theorem orcoms

Description: Commutation of disjuncts in antecedent. (Contributed by NM, 2-Dec-2012)

	Ref	Expression
Hypothesis	orcoms.1	|- ( ( ph \/ ps ) -> ch )
Assertion	orcoms	|- ( ( ps \/ ph ) -> ch )

Proof

Step	Hyp	Ref	Expression
1		orcoms.1	|- ( ( ph \/ ps ) -> ch )
2		pm1.4	|- ( ( ps \/ ph ) -> ( ph \/ ps ) )
3	2 1	syl	|- ( ( ps \/ ph ) -> ch )