Theorem rblem7

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

Hypothesis
rblem7.1
\( \vdash \neg (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \psi \vee \varphi)) \)
Conclusion
\( \vdash \neg \psi \vee \varphi \)
Proof
l0
rblem7.1
\( \vdash \neg (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \psi \vee \varphi)) \)
l1
rb-ax3
\( \vdash \neg \neg (\neg \psi \vee \varphi) \vee (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \psi \vee \varphi)) \)
rblem5
\( \vdash \neg (\neg \neg (\neg \psi \vee \varphi) \vee (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \psi \vee \varphi))) \vee (\neg \neg (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \psi \vee \varphi)) \vee (\neg \psi \vee \varphi)) \)
anmp l1 _
\( \vdash \neg \neg (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \psi \vee \varphi)) \vee (\neg \psi \vee \varphi) \)
anmp l0 _