Proof of Theorem jm2.27
Step | Hyp | Ref
| Expression |
1 | | simpl1 1064 |
. . . . . . 7
Yrm
|
2 | | simpl2 1065 |
. . . . . . 7
Yrm
|
3 | | simpl3 1066 |
. . . . . . 7
Yrm
|
4 | | simpr 477 |
. . . . . . 7
Yrm
Yrm |
5 | | eqid 2622 |
. . . . . . 7
Xrm Xrm |
6 | | eqid 2622 |
. . . . . . 7
Yrm Yrm |
7 | | eqid 2622 |
. . . . . . 7
Yrm Yrm
Yrm Yrm |
8 | | eqid 2622 |
. . . . . . 7
Xrm Yrm
Xrm Yrm |
9 | | eqid 2622 |
. . . . . . 7
Xrm
Yrm Xrm Yrm Xrm
Yrm
Xrm Yrm |
10 | | eqid 2622 |
. . . . . . 7
Xrm Yrm Xrm
Yrm Yrm
Xrm Yrm Xrm
Yrm Yrm |
11 | | eqid 2622 |
. . . . . . 7
Xrm Yrm Xrm
Yrm Xrm
Xrm Yrm Xrm
Yrm Xrm |
12 | | eqid 2622 |
. . . . . . 7
Yrm Yrm Yrm Yrm |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | jm2.27c 37574 |
. . . . . 6
Yrm
Xrm
Yrm
Yrm
Xrm
Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm
Xrm Yrm Xrm
Yrm Xrm
Yrm
Yrm
Xrm Xrm Yrm Yrm
Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Yrm Yrm
Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm Xrm Yrm Xrm
Yrm
Yrm |
14 | 13 | simpld 475 |
. . . . 5
Yrm
Xrm
Yrm Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm Yrm Xrm
Yrm
Yrm
Xrm Yrm Xrm
Yrm Xrm |
15 | 14 | simpld 475 |
. . . 4
Yrm
Xrm
Yrm Yrm
Xrm Yrm |
16 | 14 | simprd 479 |
. . . . 5
Yrm
Xrm Yrm Xrm
Yrm
Xrm
Yrm
Xrm Yrm Yrm Xrm Yrm Xrm
Yrm
Xrm |
17 | 13 | simprd 479 |
. . . . . 6
Yrm
Yrm
Yrm
Xrm Xrm Yrm Yrm
Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Yrm Yrm
Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm Xrm Yrm Xrm
Yrm
Yrm |
18 | | oveq1 6657 |
. . . . . . . . . . . 12
Yrm
Yrm
Yrm Yrm |
19 | 18 | oveq1d 6665 |
. . . . . . . . . . 11
Yrm
Yrm Yrm
Yrm |
20 | 19 | eqeq2d 2632 |
. . . . . . . . . 10
Yrm
Yrm
Yrm Yrm
Yrm Yrm
Yrm Yrm |
21 | 20 | 3anbi2d 1404 |
. . . . . . . . 9
Yrm
Yrm Xrm
Yrm
Xrm Yrm Xrm Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm
Xrm Yrm Xrm Yrm Xrm
Yrm
Xrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Xrm Yrm Yrm Yrm Yrm
Yrm Yrm Xrm Yrm Xrm Yrm Xrm
Yrm |
22 | 21 | anbi2d 740 |
. . . . . . . 8
Yrm
Yrm
Xrm Xrm Yrm Yrm
Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm
Xrm Yrm
Xrm
Xrm Yrm Yrm
Yrm Xrm
Yrm Xrm Yrm
Xrm
Yrm Xrm Yrm Xrm
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm Yrm
Yrm Yrm
Yrm Xrm Yrm Xrm Yrm Xrm
Yrm |
23 | 22 | anbi1d 741 |
. . . . . . 7
Yrm
Yrm Xrm Xrm Yrm Yrm
Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm Xrm Yrm Xrm
Yrm
Yrm Xrm Xrm Yrm Yrm
Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Yrm Yrm
Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm Xrm Yrm Xrm
Yrm
Yrm |
24 | 23 | rspcev 3309 |
. . . . . 6
Yrm Yrm
Xrm Xrm Yrm Yrm
Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Yrm Yrm
Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm Xrm Yrm Xrm
Yrm
Yrm
Xrm
Xrm Yrm Yrm
Yrm Xrm
Yrm Xrm Yrm
Xrm
Yrm Xrm Yrm Xrm
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm Yrm
Yrm Xrm Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Yrm Xrm
Yrm Xrm Yrm Yrm |
25 | 17, 24 | syl 17 |
. . . . 5
Yrm
Xrm
Xrm Yrm Yrm
Yrm Xrm
Yrm Xrm Yrm
Xrm
Yrm Xrm Yrm Xrm
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm Yrm
Yrm Xrm Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Yrm Xrm
Yrm Xrm Yrm Yrm |
26 | | eleq1 2689 |
. . . . . . . . . 10
Xrm Yrm Xrm
Yrm
Xrm
Yrm Xrm Yrm |
27 | 26 | 3anbi3d 1405 |
. . . . . . . . 9
Xrm Yrm Xrm
Yrm Xrm Xrm
Yrm Yrm Yrm
Xrm Xrm Yrm Yrm
Yrm Xrm
Yrm
Xrm Yrm |
28 | | oveq1 6657 |
. . . . . . . . . . . . . 14
Xrm Yrm Xrm
Yrm Xrm
Yrm Xrm Yrm |
29 | 28 | oveq1d 6665 |
. . . . . . . . . . . . 13
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm |
30 | 29 | oveq1d 6665 |
. . . . . . . . . . . 12
Xrm Yrm Xrm
Yrm Xrm
Yrm
Xrm Yrm |
31 | 30 | oveq2d 6666 |
. . . . . . . . . . 11
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm |
32 | 31 | eqeq1d 2624 |
. . . . . . . . . 10
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm |
33 | | oveq1 6657 |
. . . . . . . . . . 11
Xrm Yrm Xrm
Yrm Xrm
Yrm Xrm Yrm |
34 | 33 | breq2d 4665 |
. . . . . . . . . 10
Xrm Yrm Xrm
Yrm
Xrm Yrm
Xrm Yrm Xrm Yrm Xrm
Yrm |
35 | 32, 34 | 3anbi13d 1401 |
. . . . . . . . 9
Xrm Yrm Xrm
Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm
Xrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm
Yrm |
36 | 27, 35 | anbi12d 747 |
. . . . . . . 8
Xrm Yrm Xrm
Yrm
Xrm Xrm Yrm Yrm
Yrm Yrm
Yrm Xrm
Yrm
Xrm
Xrm Yrm Yrm
Yrm Xrm
Yrm Xrm Yrm
Xrm Yrm Xrm
Yrm Yrm
Yrm Xrm Yrm Xrm Yrm Xrm
Yrm |
37 | | oveq1 6657 |
. . . . . . . . . . 11
Xrm Yrm Xrm
Yrm Xrm
Yrm Xrm Yrm |
38 | 37 | breq2d 4665 |
. . . . . . . . . 10
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm |
39 | 38 | anbi1d 741 |
. . . . . . . . 9
Xrm Yrm Xrm
Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm Xrm Yrm
|
40 | 39 | anbi1d 741 |
. . . . . . . 8
Xrm Yrm Xrm
Yrm Xrm Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm
|
41 | 36, 40 | anbi12d 747 |
. . . . . . 7
Xrm Yrm Xrm
Yrm Xrm Xrm Yrm Yrm
Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm Xrm Xrm Yrm Yrm
Yrm Xrm
Yrm
Xrm Yrm
Xrm Yrm Xrm
Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm |
42 | 41 | rexbidv 3052 |
. . . . . 6
Xrm Yrm Xrm
Yrm
Xrm Xrm Yrm Yrm
Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm
Xrm Xrm Yrm Yrm
Yrm Xrm
Yrm
Xrm Yrm
Xrm Yrm Xrm
Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm |
43 | | oveq1 6657 |
. . . . . . . . . . . . 13
Xrm
Yrm Xrm Yrm Yrm Xrm Yrm Xrm
Yrm
Yrm |
44 | 43 | oveq2d 6666 |
. . . . . . . . . . . 12
Xrm
Yrm Xrm Yrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Xrm Yrm Yrm |
45 | 44 | oveq2d 6666 |
. . . . . . . . . . 11
Xrm
Yrm Xrm Yrm Yrm
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Yrm |
46 | 45 | eqeq1d 2624 |
. . . . . . . . . 10
Xrm
Yrm Xrm Yrm Yrm Xrm
Yrm
Xrm Yrm
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm |
47 | 46 | 3anbi1d 1403 |
. . . . . . . . 9
Xrm
Yrm Xrm Yrm Yrm Xrm Yrm Xrm
Yrm Yrm
Yrm Xrm Yrm Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm
Xrm Yrm |
48 | 47 | anbi2d 740 |
. . . . . . . 8
Xrm
Yrm Xrm Yrm Yrm Xrm
Xrm Yrm Yrm
Yrm Xrm
Yrm Xrm Yrm
Xrm Yrm Xrm
Yrm Yrm
Yrm Xrm Yrm Xrm Yrm Xrm
Yrm
Xrm
Xrm Yrm Yrm
Yrm Xrm
Yrm Xrm Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm
Xrm Yrm |
49 | | oveq1 6657 |
. . . . . . . . . . 11
Xrm
Yrm Xrm Yrm Yrm Xrm Yrm Xrm
Yrm
Yrm |
50 | 49 | breq2d 4665 |
. . . . . . . . . 10
Xrm
Yrm Xrm Yrm Yrm Xrm Yrm
Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm |
51 | 50 | anbi2d 740 |
. . . . . . . . 9
Xrm
Yrm Xrm Yrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Xrm
Yrm Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Yrm |
52 | | oveq1 6657 |
. . . . . . . . . . 11
Xrm
Yrm Xrm Yrm Yrm Xrm Yrm Xrm
Yrm
Yrm |
53 | 52 | breq2d 4665 |
. . . . . . . . . 10
Xrm
Yrm Xrm Yrm Yrm
Xrm Yrm Xrm
Yrm
Yrm |
54 | 53 | anbi1d 741 |
. . . . . . . . 9
Xrm
Yrm Xrm Yrm Yrm
Xrm Yrm Xrm
Yrm Yrm |
55 | 51, 54 | anbi12d 747 |
. . . . . . . 8
Xrm
Yrm Xrm Yrm Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Yrm
Xrm
Yrm
Xrm Yrm Yrm
|
56 | 48, 55 | anbi12d 747 |
. . . . . . 7
Xrm
Yrm Xrm Yrm Yrm Xrm Xrm
Yrm Yrm Yrm
Xrm Yrm Xrm
Yrm Xrm
Yrm Xrm Yrm
Yrm Yrm
Xrm Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm
Xrm Xrm
Yrm Yrm Yrm
Xrm Yrm Xrm
Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Xrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Yrm Xrm
Yrm Xrm Yrm Yrm |
57 | 56 | rexbidv 3052 |
. . . . . 6
Xrm
Yrm Xrm Yrm Yrm Xrm
Xrm Yrm Yrm
Yrm Xrm
Yrm Xrm Yrm
Xrm Yrm Xrm
Yrm Yrm
Yrm Xrm Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm Xrm Yrm
Xrm Xrm Yrm Yrm
Yrm Xrm
Yrm
Xrm Yrm
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm Yrm
Yrm Xrm Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Yrm Xrm
Yrm Xrm Yrm Yrm |
58 | | oveq1 6657 |
. . . . . . . . . . . 12
Xrm
Yrm Xrm Yrm Xrm Xrm Yrm Xrm
Yrm
Xrm |
59 | 58 | oveq1d 6665 |
. . . . . . . . . . 11
Xrm
Yrm Xrm Yrm Xrm
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm Xrm
Yrm
Xrm Yrm Xrm Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Yrm |
60 | 59 | eqeq1d 2624 |
. . . . . . . . . 10
Xrm
Yrm Xrm Yrm Xrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Xrm Yrm Yrm Xrm
Yrm Xrm Yrm Xrm
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm |
61 | 60 | 3anbi1d 1403 |
. . . . . . . . 9
Xrm
Yrm Xrm Yrm Xrm Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm
Xrm Yrm Xrm Yrm Xrm
Yrm
Xrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Xrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm
Yrm |
62 | 61 | anbi2d 740 |
. . . . . . . 8
Xrm
Yrm Xrm Yrm Xrm Xrm
Xrm Yrm Yrm
Yrm Xrm
Yrm Xrm Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm
Xrm Yrm
Xrm
Xrm Yrm Yrm
Yrm Xrm
Yrm Xrm Yrm
Xrm
Yrm Xrm Yrm Xrm
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm Yrm
Yrm Xrm Yrm Xrm Yrm Xrm
Yrm |
63 | 62 | anbi1d 741 |
. . . . . . 7
Xrm
Yrm Xrm Yrm Xrm Xrm Xrm
Yrm Yrm Yrm
Xrm Yrm Xrm
Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Xrm Yrm Yrm Yrm Yrm Xrm Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Yrm Xrm
Yrm Xrm Yrm Yrm Xrm
Xrm Yrm Yrm
Yrm Xrm
Yrm Xrm Yrm
Xrm
Yrm Xrm Yrm Xrm
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm Yrm
Yrm Xrm Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm Xrm Yrm Yrm Xrm
Yrm Xrm Yrm Yrm |
64 | 63 | rexbidv 3052 |
. . . . . 6
Xrm
Yrm Xrm Yrm Xrm Xrm
Xrm Yrm Yrm
Yrm Xrm
Yrm Xrm Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm Xrm Yrm Xrm
Yrm
Yrm
Xrm Xrm Yrm Yrm
Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm Xrm Yrm Xrm
Yrm
Yrm |
65 | 42, 57, 64 | rspc3ev 3326 |
. . . . 5
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm
Xrm Yrm Xrm
Yrm Xrm Xrm Xrm Yrm Yrm
Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm
Xrm Yrm Xrm
Yrm Xrm Yrm Xrm
Yrm
Yrm Xrm Yrm Xrm
Yrm
Yrm
Xrm Xrm Yrm Yrm
Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm |
66 | 16, 25, 65 | syl2anc 693 |
. . . 4
Yrm
Xrm Xrm Yrm Yrm
Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm |
67 | | oveq1 6657 |
. . . . . . . . . . . 12
Xrm
Xrm |
68 | 67 | oveq1d 6665 |
. . . . . . . . . . 11
Xrm
Xrm |
69 | 68 | eqeq1d 2624 |
. . . . . . . . . 10
Xrm Xrm |
70 | 69 | 3anbi1d 1403 |
. . . . . . . . 9
Xrm
Xrm |
71 | 70 | anbi1d 741 |
. . . . . . . 8
Xrm
Xrm
|
72 | 71 | anbi1d 741 |
. . . . . . 7
Xrm Xrm |
73 | 72 | 2rexbidv 3057 |
. . . . . 6
Xrm
Xrm |
74 | 73 | 2rexbidv 3057 |
. . . . 5
Xrm
Xrm
|
75 | | oveq1 6657 |
. . . . . . . . . . . . 13
Yrm
Yrm Yrm Yrm |
76 | 75 | oveq2d 6666 |
. . . . . . . . . . . 12
Yrm
Yrm Yrm
Yrm |
77 | 76 | oveq2d 6666 |
. . . . . . . . . . 11
Yrm
Yrm
Yrm Yrm |
78 | 77 | eqeq1d 2624 |
. . . . . . . . . 10
Yrm
Yrm Yrm Yrm |
79 | 78 | 3anbi2d 1404 |
. . . . . . . . 9
Yrm
Yrm Xrm
Xrm Yrm
Yrm |
80 | | eqeq1 2626 |
. . . . . . . . . 10
Yrm
Yrm
Yrm Yrm |
81 | 80 | 3anbi2d 1404 |
. . . . . . . . 9
Yrm
Yrm Yrm Yrm |
82 | 79, 81 | anbi12d 747 |
. . . . . . . 8
Yrm
Yrm
Xrm
Xrm Yrm
Yrm
Yrm
Yrm |
83 | 82 | anbi1d 741 |
. . . . . . 7
Yrm
Yrm Xrm Xrm Yrm
Yrm Yrm
Yrm |
84 | 83 | 2rexbidv 3057 |
. . . . . 6
Yrm
Yrm
Xrm
Xrm Yrm
Yrm Yrm
Yrm |
85 | 84 | 2rexbidv 3057 |
. . . . 5
Yrm
Yrm
Xrm
Xrm Yrm
Yrm
Yrm
Yrm
|
86 | | oveq1 6657 |
. . . . . . . . . . . 12
Xrm
Yrm Xrm Yrm |
87 | 86 | oveq1d 6665 |
. . . . . . . . . . 11
Xrm
Yrm Yrm Yrm Xrm
Yrm
Yrm Yrm |
88 | 87 | eqeq1d 2624 |
. . . . . . . . . 10
Xrm
Yrm Yrm
Yrm Xrm
Yrm Yrm Yrm |
89 | 88 | 3anbi2d 1404 |
. . . . . . . . 9
Xrm
Yrm Xrm Yrm Yrm
Xrm Xrm Yrm Yrm
Yrm |
90 | | breq1 4656 |
. . . . . . . . . 10
Xrm
Yrm
Xrm Yrm |
91 | 90 | 3anbi3d 1405 |
. . . . . . . . 9
Xrm
Yrm Yrm
Yrm Yrm Yrm Xrm Yrm |
92 | 89, 91 | anbi12d 747 |
. . . . . . . 8
Xrm
Yrm
Xrm Yrm
Yrm Yrm
Yrm
Xrm
Xrm Yrm Yrm
Yrm
Yrm
Yrm Xrm Yrm |
93 | | breq1 4656 |
. . . . . . . . . 10
Xrm
Yrm
Xrm Yrm
|
94 | 93 | anbi2d 740 |
. . . . . . . . 9
Xrm
Yrm Xrm Yrm
|
95 | 94 | anbi1d 741 |
. . . . . . . 8
Xrm
Yrm
Xrm Yrm
|
96 | 92, 95 | anbi12d 747 |
. . . . . . 7
Xrm
Yrm Xrm Yrm
Yrm Yrm
Yrm Xrm Xrm Yrm Yrm
Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm |
97 | 96 | 2rexbidv 3057 |
. . . . . 6
Xrm
Yrm
Xrm Yrm
Yrm Yrm
Yrm
Xrm Xrm Yrm Yrm
Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm |
98 | 97 | 2rexbidv 3057 |
. . . . 5
Xrm
Yrm
Xrm Yrm
Yrm
Yrm
Yrm
Xrm
Xrm Yrm Yrm
Yrm
Yrm
Yrm Xrm Yrm Xrm Yrm
|
99 | 74, 85, 98 | rspc3ev 3326 |
. . . 4
Xrm
Yrm
Yrm
Xrm
Yrm Xrm Xrm Yrm Yrm
Yrm Yrm
Yrm Xrm
Yrm Xrm
Yrm
|
100 | 15, 66, 99 | syl2anc 693 |
. . 3
Yrm
|
101 | 100 | ex 450 |
. 2
Yrm
|
102 | | simpll1 1100 |
. . . . . . . . 9
|
103 | 102 | ad3antrrr 766 |
. . . . . . . 8
|
104 | | simpll2 1101 |
. . . . . . . . 9
|
105 | 104 | ad3antrrr 766 |
. . . . . . . 8
|
106 | | simpll3 1102 |
. . . . . . . . 9
|
107 | 106 | ad3antrrr 766 |
. . . . . . . 8
|
108 | | simplrl 800 |
. . . . . . . . 9
|
109 | 108 | ad3antrrr 766 |
. . . . . . . 8
|
110 | | simplrr 801 |
. . . . . . . . 9
|
111 | 110 | ad3antrrr 766 |
. . . . . . . 8
|
112 | | simprl 794 |
. . . . . . . . 9
|
113 | 112 | ad3antrrr 766 |
. . . . . . . 8
|
114 | | simprr 796 |
. . . . . . . . 9
|
115 | 114 | ad3antrrr 766 |
. . . . . . . 8
|
116 | | simprl 794 |
. . . . . . . . 9
|
117 | 116 | ad2antrr 762 |
. . . . . . . 8
|
118 | | simprr 796 |
. . . . . . . . 9
|
119 | 118 | ad2antrr 762 |
. . . . . . . 8
|
120 | | simplr 792 |
. . . . . . . 8
|
121 | | simp2l1 1160 |
. . . . . . . . 9
|
122 | 121 | 3expb 1266 |
. . . . . . . 8
|
123 | | simp2l2 1161 |
. . . . . . . . 9
|
124 | 123 | 3expb 1266 |
. . . . . . . 8
|
125 | | simp2l3 1162 |
. . . . . . . . 9
|
126 | 125 | 3expb 1266 |
. . . . . . . 8
|
127 | | simp2r1 1163 |
. . . . . . . . 9
|
128 | 127 | 3expb 1266 |
. . . . . . . 8
|
129 | | simp2r2 1164 |
. . . . . . . . 9
|
130 | 129 | 3expb 1266 |
. . . . . . . 8
|
131 | | simp2r3 1165 |
. . . . . . . . 9
|
132 | 131 | 3expb 1266 |
. . . . . . . 8
|
133 | | simp3ll 1132 |
. . . . . . . . 9
|
134 | 133 | 3expb 1266 |
. . . . . . . 8
|
135 | | simp3lr 1133 |
. . . . . . . . 9
|
136 | 135 | 3expb 1266 |
. . . . . . . 8
|
137 | | simp3rl 1134 |
. . . . . . . . 9
|
138 | 137 | 3expb 1266 |
. . . . . . . 8
|
139 | | simp3rr 1135 |
. . . . . . . . 9
|
140 | 139 | 3expb 1266 |
. . . . . . . 8
|
141 | 103, 105,
107, 109, 111, 113, 115, 117, 119, 120, 122, 124, 126, 128, 130, 132, 134, 136, 138, 140 | jm2.27b 37573 |
. . . . . . 7
Yrm |
142 | 141 | ex 450 |
. . . . . 6
Yrm |
143 | 142 | rexlimdva 3031 |
. . . . 5
Yrm |
144 | 143 | rexlimdvva 3038 |
. . . 4
Yrm |
145 | 144 | rexlimdvva 3038 |
. . 3
Yrm |
146 | 145 | rexlimdvva 3038 |
. 2
Yrm |
147 | 101, 146 | impbid 202 |
1
Yrm |