Theorem rb-ax2

The second of four axioms in the Russell-Bernays axiom system. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \neg (\varphi \vee \psi) \vee (\psi \vee \varphi) \)
Proof
pm1.4
con3i _
con1i _
orri _