Theorem rblem7

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

	Ref	Expression
Hypothesis	rblem7.1	$$⊢\neg \left(\neg \left(\neg \phi \vee \psi \right)\vee \neg \left(\neg \psi \vee \phi \right)\right)$$
Assertion	rblem7	$$⊢\left(\neg \psi \vee \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		rblem7.1	$$⊢\neg \left(\neg \left(\neg \phi \vee \psi \right)\vee \neg \left(\neg \psi \vee \phi \right)\right)$$
2		rb-ax3	$$⊢\left(\neg \neg \left(\neg \psi \vee \phi \right)\vee \left(\neg \left(\neg \phi \vee \psi \right)\vee \neg \left(\neg \psi \vee \phi \right)\right)\right)$$
3		rblem5	$$⊢\left(\neg \left(\neg \neg \left(\neg \psi \vee \phi \right)\vee \left(\neg \left(\neg \phi \vee \psi \right)\vee \neg \left(\neg \psi \vee \phi \right)\right)\right)\vee \left(\neg \neg \left(\neg \left(\neg \phi \vee \psi \right)\vee \neg \left(\neg \psi \vee \phi \right)\right)\vee \left(\neg \psi \vee \phi \right)\right)\right)$$
4	2 3	anmp	$$⊢\left(\neg \neg \left(\neg \left(\neg \phi \vee \psi \right)\vee \neg \left(\neg \psi \vee \phi \right)\right)\vee \left(\neg \psi \vee \phi \right)\right)$$
5	1 4	anmp	$$⊢\left(\neg \psi \vee \phi \right)$$