re2luk1 - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > re2luk1		Unicode version

Theorem re2luk1 1530

Description: luk-1 1420 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 1515	. . . 4 $\/$ $\/$ $\/$ $\/$ $\/$
2	1	rblem7 1528	. . 3 $\/$ $\/$
3		rb-imdf 1515	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$
4	3	rblem6 1527	. . . . . . 7 $\/$ $\/$
5		rb-ax2 1518	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$
6		rb-ax4 1520	. . . . . . . . . 10 $\/$ $\/$
7		rb-ax3 1519	. . . . . . . . . 10 $\/$ $\/$
8	6, 7	rbsyl 1521	. . . . . . . . 9 $\/$
9		rb-ax4 1520	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$ $\/$
10		rb-ax3 1519	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$ $\/$
11	9, 10	rbsyl 1521	. . . . . . . . . 10 $\/$ $\/$ $\/$
12		rb-ax2 1518	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
13	11, 12	anmp 1516	. . . . . . . . 9 $\/$ $\/$ $\/$
14	8, 13	rblem1 1522	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$
15	5, 14	rbsyl 1521	. . . . . . 7 $\/$ $\/$ $\/$ $\/$ $\/$
16	4, 15	anmp 1516	. . . . . 6 $\/$ $\/$
17		rb-imdf 1515	. . . . . . 7 $\/$ $\/$ $\/$ $\/$ $\/$
18	17	rblem7 1528	. . . . . 6 $\/$ $\/$
19	16, 18	rblem1 1522	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$
20		rb-ax1 1517	. . . . . 6 $\/$ $\/$ $\/$ $\/$ $\/$
21		rb-ax2 1518	. . . . . . 7 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
22		rb-ax4 1520	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$ $\/$
23		rb-ax3 1519	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$ $\/$
24	22, 23	rbsyl 1521	. . . . . . . . 9 $\/$ $\/$ $\/$
25		rb-ax4 1520	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$ $\/$
26		rb-ax3 1519	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$ $\/$
27	25, 26	rbsyl 1521	. . . . . . . . 9 $\/$ $\/$ $\/$
28	24, 27, 11	rblem4 1525	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
29		rb-ax2 1518	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
30	28, 29	rbsyl 1521	. . . . . . 7 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
31	21, 30	rbsyl 1521	. . . . . 6 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
32	20, 31	anmp 1516	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$
33	19, 32	rbsyl 1521	. . . 4 $\/$ $\/$ $\/$
34		rb-imdf 1515	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$
35	34	rblem6 1527	. . . 4 $\/$ $\/$
36	33, 35	rbsyl 1521	. . 3 $\/$ $\/$
37	2, 36	rbsyl 1521	. 2 $\/$
38		rb-imdf 1515	. . 3 $\/$ $\/$ $\/$ $\/$ $\/$
39	38	rblem7 1528	. 2 $\/$ $\/$
40	37, 39	anmp 1516	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $\/$ wo 357

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 177 df-or 359 df-an 360

This theorem is referenced by: (None)

W3C validator