Theorem
or12
Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
Conclusion
\( \vdash \varphi \vee (\psi \vee \chi) \leftrightarrow \psi \vee (\varphi \vee \chi) \)
Proof
l0
pm1.5
pm1.5
impbii
l0
_
This is the content in the right pane.