Theorem orcom

Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 15-Nov-2012.)

Conclusion
\( \vdash \varphi \vee \psi \leftrightarrow \psi \vee \varphi \)
Proof
l0
pm1.4
pm1.4
impbii l0 _