Theorem rbsyl

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

Hypotheses
rbsyl.1
\( \vdash \neg \psi \vee \chi \)
rbsyl.2
\( \vdash \varphi \vee \psi \)
Conclusion
\( \vdash \varphi \vee \chi \)
Proof
l0
rbsyl.2
\( \vdash \varphi \vee \psi \)
l1
rbsyl.1
\( \vdash \neg \psi \vee \chi \)
rb-ax1
\( \vdash \neg (\neg \psi \vee \chi) \vee (\neg (\varphi \vee \psi) \vee (\varphi \vee \chi)) \)
anmp l1 _
\( \vdash \neg (\varphi \vee \psi) \vee (\varphi \vee \chi) \)
anmp l0 _