Theorem rblem3

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

Proof

Step	Hyp	Ref	Expression
1		rb-ax2	|- ( -. ( ph \/ ( ch \/ ps ) ) \/ ( ( ch \/ ps ) \/ ph ) )
2		rblem2	|- ( -. ( ph \/ ch ) \/ ( ph \/ ( ch \/ ps ) ) )
3		rb-ax2	|- ( -. ( ch \/ ph ) \/ ( ph \/ ch ) )
4	2 3	rbsyl	|- ( -. ( ch \/ ph ) \/ ( ph \/ ( ch \/ ps ) ) )
5	1 4	rbsyl	|- ( -. ( ch \/ ph ) \/ ( ( ch \/ ps ) \/ ph ) )