Theorem rb-ax1

The first 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 (\neg \psi \vee \chi) \vee (\neg (\varphi \vee \psi) \vee (\varphi \vee \chi)) \)
Proof
l0
orim2
\( \vdash (\psi \rightarrow \chi) \rightarrow \varphi \vee \psi \rightarrow \varphi \vee \chi \)
l1
imor
\( \vdash \psi \rightarrow \chi \leftrightarrow \neg \psi \vee \chi \)
imor
\( \vdash \varphi \vee \psi \rightarrow \varphi \vee \chi \leftrightarrow \neg (\varphi \vee \psi) \vee (\varphi \vee \chi) \)
3imtr3i l0 l1 _
imori _