![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > lcfrlem25 | Structured version Visualization version Unicode version |
Description: Lemma for lcfr 35154. Special case of lcfrlem35 35146 when
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
lcfrlem17.h |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem17.o |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem17.u |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem17.v |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem17.p |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem17.z |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem17.n |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem17.a |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem17.k |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem17.x |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem17.y |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem17.ne |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem22.b |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem24.t |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem24.s |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem24.q |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem24.r |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem24.j |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem24.ib |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem24.l |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem25.d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem25.jz |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem25.in |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
lcfrlem25 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lcfrlem17.h |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | lcfrlem17.o |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | lcfrlem17.u |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | lcfrlem17.v |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | lcfrlem17.p |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | lcfrlem17.z |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | lcfrlem17.n |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | lcfrlem17.a |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | lcfrlem17.k |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | lcfrlem17.x |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | lcfrlem17.y |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
12 | lcfrlem17.ne |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
13 | lcfrlem22.b |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
14 | eqid 2451 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
15 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14 | lcfrlem23 35134 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | lcfrlem24.t |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
17 | lcfrlem24.s |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
18 | lcfrlem24.q |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
19 | lcfrlem24.r |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
20 | lcfrlem24.j |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
21 | lcfrlem24.ib |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
22 | lcfrlem24.l |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
23 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 16, 17, 18, 19, 20, 21, 22 | lcfrlem24 35135 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
24 | inss2 3620 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
25 | 23, 24 | syl6eqss 3449 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
26 | 1, 3, 9 | dvhlvec 34678 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
27 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13 | lcfrlem22 35133 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
28 | lcfrlem25.in |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
29 | 6, 7, 8, 26, 27, 21, 28 | lsatel 32572 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
30 | eqid 2451 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
31 | 1, 3, 9 | dvhlmod 34679 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
32 | eqid 2451 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
33 | lcfrlem25.d |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
34 | eqid 2451 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
35 | eqid 2451 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
36 | 1, 2, 3, 4, 5, 16, 17, 19, 6, 32, 22, 33, 34, 35, 20, 9, 11 | lcfrlem10 35121 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
37 | 32, 22, 30 | lkrlss 32662 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
38 | 31, 36, 37 | syl2anc 671 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
39 | lcfrlem25.jz |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
40 | 4, 8, 31, 27 | lsatssv 32565 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
41 | 40, 21 | sseldd 3400 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
42 | 4, 17, 18, 32, 22, 31, 36, 41 | ellkr2 32658 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
43 | 39, 42 | mpbird 240 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
44 | 30, 7, 31, 38, 43 | lspsnel5a 18229 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
45 | 29, 44 | eqsstrd 3433 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
46 | 30 | lsssssubg 18191 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
47 | 31, 46 | syl 17 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
48 | 10 | eldifad 3383 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
49 | 11 | eldifad 3383 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
50 | prssi 4096 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
51 | 48, 49, 50 | syl2anc 671 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
52 | 1, 3, 4, 30, 2 | dochlss 34923 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
53 | 9, 51, 52 | syl2anc 671 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
54 | 47, 53 | sseldd 3400 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
55 | 4, 30, 7, 31, 48, 49 | lspprcl 18211 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
56 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 | lcfrlem17 35128 |
. . . . . . . . . . 11
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
57 | 56 | eldifad 3383 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
58 | 57 | snssd 4085 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
59 | 1, 3, 4, 30, 2 | dochlss 34923 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
60 | 9, 58, 59 | syl2anc 671 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
61 | 30 | lssincl 18198 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
62 | 31, 55, 60, 61 | syl3anc 1271 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
63 | 13, 62 | syl5eqel 2533 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
64 | 47, 63 | sseldd 3400 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
65 | 47, 38 | sseldd 3400 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
66 | 14 | lsmlub 17325 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
67 | 54, 64, 65, 66 | syl3anc 1271 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
68 | 25, 45, 67 | mpbi2and 932 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
69 | 15, 68 | eqsstr3d 3434 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
70 | eqid 2451 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
71 | 1, 2, 3, 4, 6, 70, 9, 56 | dochsnshp 35022 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
72 | 1, 2, 3, 4, 5, 16, 17, 19, 6, 32, 22, 33, 34, 35, 20, 9, 11 | lcfrlem13 35124 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
73 | eldifsni 4066 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
74 | 72, 73 | syl 17 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
75 | 70, 32, 22, 33, 34, 26, 36 | lduallkr3 32729 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
76 | 74, 75 | mpbird 240 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
77 | 70, 26, 71, 76 | lshpcmp 32555 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
78 | 69, 77 | mpbid 215 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1672 ax-4 1685 ax-5 1761 ax-6 1808 ax-7 1854 ax-8 1892 ax-9 1899 ax-10 1918 ax-11 1923 ax-12 1936 ax-13 2091 ax-ext 2431 ax-rep 4486 ax-sep 4496 ax-nul 4505 ax-pow 4553 ax-pr 4611 ax-un 6570 ax-cnex 9581 ax-resscn 9582 ax-1cn 9583 ax-icn 9584 ax-addcl 9585 ax-addrcl 9586 ax-mulcl 9587 ax-mulrcl 9588 ax-mulcom 9589 ax-addass 9590 ax-mulass 9591 ax-distr 9592 ax-i2m1 9593 ax-1ne0 9594 ax-1rid 9595 ax-rnegex 9596 ax-rrecex 9597 ax-cnre 9598 ax-pre-lttri 9599 ax-pre-lttrn 9600 ax-pre-ltadd 9601 ax-pre-mulgt0 9602 ax-riotaBAD 32526 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 987 df-3an 988 df-tru 1450 df-fal 1453 df-ex 1667 df-nf 1671 df-sb 1801 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3014 df-sbc 3235 df-csb 3331 df-dif 3374 df-un 3376 df-in 3378 df-ss 3385 df-pss 3387 df-nul 3699 df-if 3849 df-pw 3920 df-sn 3936 df-pr 3938 df-tp 3940 df-op 3942 df-uni 4168 df-int 4204 df-iun 4249 df-iin 4250 df-br 4374 df-opab 4433 df-mpt 4434 df-tr 4469 df-eprel 4722 df-id 4726 df-po 4732 df-so 4733 df-fr 4770 df-we 4772 df-xp 4817 df-rel 4818 df-cnv 4819 df-co 4820 df-dm 4821 df-rn 4822 df-res 4823 df-ima 4824 df-pred 5358 df-ord 5404 df-on 5405 df-lim 5406 df-suc 5407 df-iota 5524 df-fun 5562 df-fn 5563 df-f 5564 df-f1 5565 df-fo 5566 df-f1o 5567 df-fv 5568 df-riota 6237 df-ov 6278 df-oprab 6279 df-mpt2 6280 df-of 6518 df-om 6680 df-1st 6780 df-2nd 6781 df-tpos 6959 df-undef 7006 df-wrecs 7014 df-recs 7076 df-rdg 7114 df-1o 7168 df-oadd 7172 df-er 7349 df-map 7460 df-en 7556 df-dom 7557 df-sdom 7558 df-fin 7559 df-pnf 9663 df-mnf 9664 df-xr 9665 df-ltxr 9666 df-le 9667 df-sub 9848 df-neg 9849 df-nn 10598 df-2 10656 df-3 10657 df-4 10658 df-5 10659 df-6 10660 df-n0 10859 df-z 10927 df-uz 11149 df-fz 11775 df-struct 15133 df-ndx 15134 df-slot 15135 df-base 15136 df-sets 15137 df-ress 15138 df-plusg 15213 df-mulr 15214 df-sca 15216 df-vsca 15217 df-0g 15350 df-mre 15502 df-mrc 15503 df-acs 15505 df-preset 16183 df-poset 16201 df-plt 16214 df-lub 16230 df-glb 16231 df-join 16232 df-meet 16233 df-p0 16295 df-p1 16296 df-lat 16302 df-clat 16364 df-mgm 16498 df-sgrp 16537 df-mnd 16547 df-submnd 16593 df-grp 16683 df-minusg 16684 df-sbg 16685 df-subg 16824 df-cntz 16981 df-oppg 17007 df-lsm 17298 df-cmn 17442 df-abl 17443 df-mgp 17734 df-ur 17746 df-ring 17792 df-oppr 17861 df-dvdsr 17879 df-unit 17880 df-invr 17910 df-dvr 17921 df-drng 17987 df-lmod 18103 df-lss 18166 df-lsp 18205 df-lvec 18336 df-lsatoms 32543 df-lshyp 32544 df-lcv 32586 df-lfl 32625 df-lkr 32653 df-ldual 32691 df-oposet 32743 df-ol 32745 df-oml 32746 df-covers 32833 df-ats 32834 df-atl 32865 df-cvlat 32889 df-hlat 32918 df-llines 33064 df-lplanes 33065 df-lvols 33066 df-lines 33067 df-psubsp 33069 df-pmap 33070 df-padd 33362 df-lhyp 33554 df-laut 33555 df-ldil 33670 df-ltrn 33671 df-trl 33726 df-tgrp 34311 df-tendo 34323 df-edring 34325 df-dveca 34571 df-disoa 34598 df-dvech 34648 df-dib 34708 df-dic 34742 df-dih 34798 df-doch 34917 df-djh 34964 |
This theorem is referenced by: lcfrlem26 35137 |
Copyright terms: Public domain | W3C validator |