Theorem rblem2

Used to rederive the Lukasiewicz axioms from Russell-Bernays'. (Contributed by Anthony Hart, 18-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \neg (\chi \vee \varphi) \vee (\chi \vee (\varphi \vee \psi)) \)
Proof
l0
rb-ax2
\( \vdash \neg (\psi \vee \varphi) \vee (\varphi \vee \psi) \)
rb-ax3
\( \vdash \neg \varphi \vee (\psi \vee \varphi) \)
l2
rbsyl l0 _
\( \vdash \neg \varphi \vee (\varphi \vee \psi) \)
rb-ax1
\( \vdash \neg (\neg \varphi \vee (\varphi \vee \psi)) \vee (\neg (\chi \vee \varphi) \vee (\chi \vee (\varphi \vee \psi))) \)
anmp l2 _