Theorem orcoms

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

	Ref	Expression
Hypothesis	orcoms.1	$$⊢\left(\phi \vee \psi \right)\to \chi$$
Assertion	orcoms	$$⊢\left(\psi \vee \phi \right)\to \chi$$

Proof

Step	Hyp	Ref	Expression
1		orcoms.1	$$⊢\left(\phi \vee \psi \right)\to \chi$$
2		pm1.4	$$⊢\left(\psi \vee \phi \right)\to \left(\phi \vee \psi \right)$$
3	2 1	syl	$$⊢\left(\psi \vee \phi \right)\to \chi$$