Theorem orcomd

Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010.)

Hypothesis
orcomd.1
\( \vdash \varphi \rightarrow \psi \vee \chi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \vee \psi \)
Proof
l0
orcomd.1
\( \vdash \varphi \rightarrow \psi \vee \chi \)
orcom
\( \vdash \psi \vee \chi \leftrightarrow \chi \vee \psi \)
sylib l0 _