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	|- ( -. ph \/ ps )
	rblem1.2	|- ( -. ch \/ th )
Assertion	rblem1	|- ( -. ( ph \/ ch ) \/ ( ps \/ th ) )

Proof

Step	Hyp	Ref	Expression
1		rblem1.1	|- ( -. ph \/ ps )
2		rblem1.2	|- ( -. ch \/ th )
3		rb-ax1	|- ( -. ( -. ch \/ th ) \/ ( -. ( ps \/ ch ) \/ ( ps \/ th ) ) )
4	2 3	anmp	|- ( -. ( ps \/ ch ) \/ ( ps \/ th ) )
5		rb-ax2	|- ( -. ( ch \/ ps ) \/ ( ps \/ ch ) )
6		rb-ax1	|- ( -. ( -. ph \/ ps ) \/ ( -. ( ch \/ ph ) \/ ( ch \/ ps ) ) )
7	1 6	anmp	|- ( -. ( ch \/ ph ) \/ ( ch \/ ps ) )
8		rb-ax2	|- ( -. ( ph \/ ch ) \/ ( ch \/ ph ) )
9	7 8	rbsyl	|- ( -. ( ph \/ ch ) \/ ( ch \/ ps ) )
10	5 9	rbsyl	|- ( -. ( ph \/ ch ) \/ ( ps \/ ch ) )
11	4 10	rbsyl	|- ( -. ( ph \/ ch ) \/ ( ps \/ th ) )