Theorem rbsyl

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

Proof

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