Theorem orcoms

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

	Ref	Expression
Hypothesis	orcoms.1	⊢ ( ( 𝜑 ∨ 𝜓 ) → 𝜒 )
Assertion	orcoms	⊢ ( ( 𝜓 ∨ 𝜑 ) → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		orcoms.1	⊢ ( ( 𝜑 ∨ 𝜓 ) → 𝜒 )
2		pm1.4	⊢ ( ( 𝜓 ∨ 𝜑 ) → ( 𝜑 ∨ 𝜓 ) )
3	2 1	syl	⊢ ( ( 𝜓 ∨ 𝜑 ) → 𝜒 )