Theorem rblem5

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

Proof

Step	Hyp	Ref	Expression
1		rb-ax2	|- ( -. ( ph \/ -. -. ps ) \/ ( -. -. ps \/ ph ) )
2		rb-ax4	|- ( -. ( ph \/ ph ) \/ ph )
3		rb-ax3	|- ( -. ph \/ ( ph \/ ph ) )
4	2 3	rbsyl	|- ( -. ph \/ ph )
5		rb-ax4	|- ( -. ( -. -. ph \/ -. -. ph ) \/ -. -. ph )
6		rb-ax3	|- ( -. -. -. ph \/ ( -. -. ph \/ -. -. ph ) )
7	5 6	rbsyl	|- ( -. -. -. ph \/ -. -. ph )
8		rb-ax2	|- ( -. ( -. -. -. ph \/ -. -. ph ) \/ ( -. -. ph \/ -. -. -. ph ) )
9	7 8	anmp	|- ( -. -. ph \/ -. -. -. ph )
10	9 4	rblem1	|- ( -. ( -. ph \/ ph ) \/ ( -. -. -. ph \/ ph ) )
11	4 10	anmp	|- ( -. -. -. ph \/ ph )
12		rb-ax4	|- ( -. ( -. ps \/ -. ps ) \/ -. ps )
13		rb-ax3	|- ( -. -. ps \/ ( -. ps \/ -. ps ) )
14	12 13	rbsyl	|- ( -. -. ps \/ -. ps )
15		rb-ax2	|- ( -. ( -. -. ps \/ -. ps ) \/ ( -. ps \/ -. -. ps ) )
16	14 15	anmp	|- ( -. ps \/ -. -. ps )
17	11 16	rblem1	|- ( -. ( -. -. ph \/ ps ) \/ ( ph \/ -. -. ps ) )
18	1 17	rbsyl	|- ( -. ( -. -. ph \/ ps ) \/ ( -. -. ps \/ ph ) )