Theorem orcoms

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

Hypothesis
orcoms.1
\( \vdash \varphi \vee \psi \rightarrow \chi \)
Conclusion
\( \vdash \psi \vee \varphi \rightarrow \chi \)
Proof
l0
pm1.4
\( \vdash \psi \vee \varphi \rightarrow \varphi \vee \psi \)
orcoms.1
\( \vdash \varphi \vee \psi \rightarrow \chi \)
syl l0 _