Theorem rblem3

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 \psi \vee \varphi) \)
Proof
l0
rb-ax2
\( \vdash \neg (\varphi \vee (\chi \vee \psi)) \vee (\chi \vee \psi \vee \varphi) \)
l1
rblem2
\( \vdash \neg (\varphi \vee \chi) \vee (\varphi \vee (\chi \vee \psi)) \)
rb-ax2
\( \vdash \neg (\chi \vee \varphi) \vee (\varphi \vee \chi) \)
rbsyl l1 _
\( \vdash \neg (\chi \vee \varphi) \vee (\varphi \vee (\chi \vee \psi)) \)
rbsyl l0 _