re2luk1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > re2luk1		Structured version Visualization version Unicode version

Theorem re2luk1 1690

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

**Assertion**
Ref	Expression
re2luk1

**Proof of Theorem re2luk1**
Step	Hyp	Ref	Expression
1		rb-imdf 1675	. . . 4 $\/$ $\/$ $\/$ $\/$ $\/$
2	1	rblem7 1688	. . 3 $\/$ $\/$
3		rb-imdf 1675	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$
4	3	rblem6 1687	. . . . . . 7 $\/$ $\/$
5		rb-ax2 1678	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$
6		rb-ax4 1680	. . . . . . . . . 10 $\/$ $\/$
7		rb-ax3 1679	. . . . . . . . . 10 $\/$ $\/$
8	6, 7	rbsyl 1681	. . . . . . . . 9 $\/$
9		rb-ax4 1680	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$ $\/$
10		rb-ax3 1679	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$ $\/$
11	9, 10	rbsyl 1681	. . . . . . . . . 10 $\/$ $\/$ $\/$
12		rb-ax2 1678	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
13	11, 12	anmp 1676	. . . . . . . . 9 $\/$ $\/$ $\/$
14	8, 13	rblem1 1682	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$
15	5, 14	rbsyl 1681	. . . . . . 7 $\/$ $\/$ $\/$ $\/$ $\/$
16	4, 15	anmp 1676	. . . . . 6 $\/$ $\/$
17		rb-imdf 1675	. . . . . . 7 $\/$ $\/$ $\/$ $\/$ $\/$
18	17	rblem7 1688	. . . . . 6 $\/$ $\/$
19	16, 18	rblem1 1682	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$
20		rb-ax1 1677	. . . . . 6 $\/$ $\/$ $\/$ $\/$ $\/$
21		rb-ax2 1678	. . . . . . 7 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
22		rb-ax4 1680	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$ $\/$
23		rb-ax3 1679	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$ $\/$
24	22, 23	rbsyl 1681	. . . . . . . . 9 $\/$ $\/$ $\/$
25		rb-ax4 1680	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$ $\/$
26		rb-ax3 1679	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$ $\/$
27	25, 26	rbsyl 1681	. . . . . . . . 9 $\/$ $\/$ $\/$
28	24, 27, 11	rblem4 1685	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
29		rb-ax2 1678	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
30	28, 29	rbsyl 1681	. . . . . . 7 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
31	21, 30	rbsyl 1681	. . . . . 6 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
32	20, 31	anmp 1676	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$
33	19, 32	rbsyl 1681	. . . 4 $\/$ $\/$ $\/$
34		rb-imdf 1675	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$
35	34	rblem6 1687	. . . 4 $\/$ $\/$
36	33, 35	rbsyl 1681	. . 3 $\/$ $\/$
37	2, 36	rbsyl 1681	. 2 $\/$
38		rb-imdf 1675	. . 3 $\/$ $\/$ $\/$ $\/$ $\/$
39	38	rblem7 1688	. 2 $\/$ $\/$
40	37, 39	anmp 1676	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $\/$ wo 383

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386

This theorem is referenced by: (None)

W3C validator