Theorem re2luk2

Description: luk-2 derived from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	re2luk2	|- ( ( -. ph -> ph ) -> ph )

Proof

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