Theorem rblem1

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

	Ref	Expression
Hypotheses	rblem1.1	$$⊢\left(\neg \phi \vee \psi \right)$$
	rblem1.2	$$⊢\left(\neg \chi \vee \theta \right)$$
Assertion	rblem1	$$⊢\left(\neg \left(\phi \vee \chi \right)\vee \left(\psi \vee \theta \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		rblem1.1	$$⊢\left(\neg \phi \vee \psi \right)$$
2		rblem1.2	$$⊢\left(\neg \chi \vee \theta \right)$$
3		rb-ax1	$$⊢\left(\neg \left(\neg \chi \vee \theta \right)\vee \left(\neg \left(\psi \vee \chi \right)\vee \left(\psi \vee \theta \right)\right)\right)$$
4	2 3	anmp	$$⊢\left(\neg \left(\psi \vee \chi \right)\vee \left(\psi \vee \theta \right)\right)$$
5		rb-ax2	$$⊢\left(\neg \left(\chi \vee \psi \right)\vee \left(\psi \vee \chi \right)\right)$$
6		rb-ax1	$$⊢\left(\neg \left(\neg \phi \vee \psi \right)\vee \left(\neg \left(\chi \vee \phi \right)\vee \left(\chi \vee \psi \right)\right)\right)$$
7	1 6	anmp	$$⊢\left(\neg \left(\chi \vee \phi \right)\vee \left(\chi \vee \psi \right)\right)$$
8		rb-ax2	$$⊢\left(\neg \left(\phi \vee \chi \right)\vee \left(\chi \vee \phi \right)\right)$$
9	7 8	rbsyl	$$⊢\left(\neg \left(\phi \vee \chi \right)\vee \left(\chi \vee \psi \right)\right)$$
10	5 9	rbsyl	$$⊢\left(\neg \left(\phi \vee \chi \right)\vee \left(\psi \vee \chi \right)\right)$$
11	4 10	rbsyl	$$⊢\left(\neg \left(\phi \vee \chi \right)\vee \left(\psi \vee \theta \right)\right)$$