Theorem rblem1
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
rblem1.1
\( \vdash \neg \varphi \vee \psi \)
rblem1.2
\( \vdash \neg \chi \vee \theta \)
Conclusion
\( \vdash \neg (\varphi \vee \chi) \vee (\psi \vee \theta) \)
Proof
l0
rblem1.2
\( \vdash \neg \chi \vee \theta \)
rb-ax1
\( \vdash \neg (\neg \chi \vee \theta) \vee (\neg (\psi \vee \chi) \vee (\psi \vee \theta)) \)
l2
anmp l0 _
\( \vdash \neg (\psi \vee \chi) \vee (\psi \vee \theta) \)
l3
rb-ax2
\( \vdash \neg (\chi \vee \psi) \vee (\psi \vee \chi) \)
l4
rblem1.1
\( \vdash \neg \varphi \vee \psi \)
rb-ax1
\( \vdash \neg (\neg \varphi \vee \psi) \vee (\neg (\chi \vee \varphi) \vee (\chi \vee \psi)) \)
l6
anmp l4 _
\( \vdash \neg (\chi \vee \varphi) \vee (\chi \vee \psi) \)
rb-ax2
\( \vdash \neg (\varphi \vee \chi) \vee (\chi \vee \varphi) \)
rbsyl l6 _
\( \vdash \neg (\varphi \vee \chi) \vee (\chi \vee \psi) \)
rbsyl l3 _
\( \vdash \neg (\varphi \vee \chi) \vee (\psi \vee \chi) \)
rbsyl l2 _