Step | Hyp | Ref
| Expression |
1 | | csrg 13151 |
. 2
SRing |
2 | | vf |
. . . . . . 7
 |
3 | 2 | cv 1352 |
. . . . . 6
 |
4 | | cmgp 13135 |
. . . . . 6
mulGrp |
5 | 3, 4 | cfv 5218 |
. . . . 5
mulGrp   |
6 | | cmnd 12822 |
. . . . 5
 |
7 | 5, 6 | wcel 2148 |
. . . 4
mulGrp   |
8 | | vx |
. . . . . . . . . . . . . . . 16
 |
9 | 8 | cv 1352 |
. . . . . . . . . . . . . . 15
 |
10 | | vy |
. . . . . . . . . . . . . . . . 17
 |
11 | 10 | cv 1352 |
. . . . . . . . . . . . . . . 16
 |
12 | | vz |
. . . . . . . . . . . . . . . . 17
 |
13 | 12 | cv 1352 |
. . . . . . . . . . . . . . . 16
 |
14 | | vp |
. . . . . . . . . . . . . . . . 17
 |
15 | 14 | cv 1352 |
. . . . . . . . . . . . . . . 16
 |
16 | 11, 13, 15 | co 5877 |
. . . . . . . . . . . . . . 15
     |
17 | | vt |
. . . . . . . . . . . . . . . 16
 |
18 | 17 | cv 1352 |
. . . . . . . . . . . . . . 15
 |
19 | 9, 16, 18 | co 5877 |
. . . . . . . . . . . . . 14
         |
20 | 9, 11, 18 | co 5877 |
. . . . . . . . . . . . . . 15
     |
21 | 9, 13, 18 | co 5877 |
. . . . . . . . . . . . . . 15
     |
22 | 20, 21, 15 | co 5877 |
. . . . . . . . . . . . . 14
             |
23 | 19, 22 | wceq 1353 |
. . . . . . . . . . . . 13
                     |
24 | 9, 11, 15 | co 5877 |
. . . . . . . . . . . . . . 15
     |
25 | 24, 13, 18 | co 5877 |
. . . . . . . . . . . . . 14
         |
26 | 11, 13, 18 | co 5877 |
. . . . . . . . . . . . . . 15
     |
27 | 21, 26, 15 | co 5877 |
. . . . . . . . . . . . . 14
             |
28 | 25, 27 | wceq 1353 |
. . . . . . . . . . . . 13
                     |
29 | 23, 28 | wa 104 |
. . . . . . . . . . . 12
                                           |
30 | | vr |
. . . . . . . . . . . . 13
 |
31 | 30 | cv 1352 |
. . . . . . . . . . . 12
 |
32 | 29, 12, 31 | wral 2455 |
. . . . . . . . . . 11

                                           |
33 | 32, 10, 31 | wral 2455 |
. . . . . . . . . 10


                                           |
34 | | vn |
. . . . . . . . . . . . . 14
 |
35 | 34 | cv 1352 |
. . . . . . . . . . . . 13
 |
36 | 35, 9, 18 | co 5877 |
. . . . . . . . . . . 12
     |
37 | 36, 35 | wceq 1353 |
. . . . . . . . . . 11
     |
38 | 9, 35, 18 | co 5877 |
. . . . . . . . . . . 12
     |
39 | 38, 35 | wceq 1353 |
. . . . . . . . . . 11
     |
40 | 37, 39 | wa 104 |
. . . . . . . . . 10
           |
41 | 33, 40 | wa 104 |
. . . . . . . . 9
 

                                                      |
42 | 41, 8, 31 | wral 2455 |
. . . . . . . 8

 

                                                      |
43 | | c0g 12710 |
. . . . . . . . 9
 |
44 | 3, 43 | cfv 5218 |
. . . . . . . 8
     |
45 | 42, 34, 44 | wsbc 2964 |
. . . . . . 7
      ![]. ].](_drbrack.gif)   

                                                      |
46 | | cmulr 12539 |
. . . . . . . 8
 |
47 | 3, 46 | cfv 5218 |
. . . . . . 7
     |
48 | 45, 17, 47 | wsbc 2964 |
. . . . . 6
      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   

                                                      |
49 | | cplusg 12538 |
. . . . . . 7
 |
50 | 3, 49 | cfv 5218 |
. . . . . 6
    |
51 | 48, 14, 50 | wsbc 2964 |
. . . . 5
     ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   

                                                      |
52 | | cbs 12464 |
. . . . . 6
 |
53 | 3, 52 | cfv 5218 |
. . . . 5
     |
54 | 51, 30, 53 | wsbc 2964 |
. . . 4
      ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)                                                           |
55 | 7, 54 | wa 104 |
. . 3
 mulGrp        ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif) 
                                                          |
56 | | ccmn 13093 |
. . 3
CMnd |
57 | 55, 2, 56 | crab 2459 |
. 2
 CMnd  mulGrp        ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif) 
                                                           |
58 | 1, 57 | wceq 1353 |
1
SRing  CMnd
 mulGrp        ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)                                                             |