Theorem rblem6

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	rblem6.1	|- -. ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) )
Assertion	rblem6	|- ( -. ph \/ ps )

Proof

Step	Hyp	Ref	Expression
1		rblem6.1	|- -. ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) )
2		rb-ax4	|- ( -. ( -. ( -. ph \/ ps ) \/ -. ( -. ph \/ ps ) ) \/ -. ( -. ph \/ ps ) )
3		rb-ax3	|- ( -. -. ( -. ph \/ ps ) \/ ( -. ( -. ph \/ ps ) \/ -. ( -. ph \/ ps ) ) )
4	2 3	rbsyl	|- ( -. -. ( -. ph \/ ps ) \/ -. ( -. ph \/ ps ) )
5		rb-ax2	|- ( -. ( -. -. ( -. ph \/ ps ) \/ -. ( -. ph \/ ps ) ) \/ ( -. ( -. ph \/ ps ) \/ -. -. ( -. ph \/ ps ) ) )
6	4 5	anmp	|- ( -. ( -. ph \/ ps ) \/ -. -. ( -. ph \/ ps ) )
7		rblem3	|- ( -. ( -. ( -. ph \/ ps ) \/ -. -. ( -. ph \/ ps ) ) \/ ( ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) \/ -. -. ( -. ph \/ ps ) ) )
8	6 7	anmp	|- ( ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) \/ -. -. ( -. ph \/ ps ) )
9		rb-ax2	|- ( -. ( ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) \/ -. -. ( -. ph \/ ps ) ) \/ ( -. -. ( -. ph \/ ps ) \/ ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) ) )
10	8 9	anmp	|- ( -. -. ( -. ph \/ ps ) \/ ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) )
11		rblem5	|- ( -. ( -. -. ( -. ph \/ ps ) \/ ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) ) \/ ( -. -. ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) \/ ( -. ph \/ ps ) ) )
12	10 11	anmp	|- ( -. -. ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) \/ ( -. ph \/ ps ) )
13	1 12	anmp	|- ( -. ph \/ ps )