Step | Hyp | Ref
| Expression |
1 | | oveq1 5878 |
. . . . . . 7
                   |
2 | 1 | adantl 277 |
. . . . . 6
                     |
3 | 2 | 3ad2ant2 1019 |
. . . . 5
  
                          |
4 | | df-3an 980 |
. . . . . . . . 9
 
  

   |
5 | | caovimo.ass |
. . . . . . . . . . . . . 14
 
                   |
6 | 5 | adantl 277 |
. . . . . . . . . . . . 13
  


                    |
7 | | simp1 997 |
. . . . . . . . . . . . 13
 
   |
8 | | simp2 998 |
. . . . . . . . . . . . 13
 
   |
9 | | simp3 999 |
. . . . . . . . . . . . 13
 
   |
10 | 6, 7, 8, 9 | caovassd 6030 |
. . . . . . . . . . . 12
 
                   |
11 | | caovimo.com |
. . . . . . . . . . . . . 14
 
           |
12 | 11 | adantl 277 |
. . . . . . . . . . . . 13
  


            |
13 | 7, 8, 9, 12, 6 | caov12d 6052 |
. . . . . . . . . . . 12
 
                   |
14 | 10, 13 | eqtrd 2210 |
. . . . . . . . . . 11
 
                   |
15 | 14 | adantr 276 |
. . . . . . . . . 10
  

                       |
16 | | oveq2 5879 |
. . . . . . . . . . . 12
                   |
17 | | oveq1 5878 |
. . . . . . . . . . . . . 14
           |
18 | | id 19 |
. . . . . . . . . . . . . 14
   |
19 | 17, 18 | eqeq12d 2192 |
. . . . . . . . . . . . 13
     
       |
20 | | caovimo.id |
. . . . . . . . . . . . 13
       |
21 | 19, 20 | vtoclga 2803 |
. . . . . . . . . . . 12
       |
22 | 16, 21 | sylan9eqr 2232 |
. . . . . . . . . . 11
                 |
23 | 22 | 3ad2antl2 1160 |
. . . . . . . . . 10
  

               |
24 | 15, 23 | eqtrd 2210 |
. . . . . . . . 9
  

               |
25 | 4, 24 | sylanbr 285 |
. . . . . . . 8
                     |
26 | 25 | anasss 399 |
. . . . . . 7
  


                |
27 | 26 | 3impa 1194 |
. . . . . 6
 
      
          |
28 | 27 | 3adant2r 1233 |
. . . . 5
  
                      |
29 | 11 | adantl 277 |
. . . . . . . . 9
  
            |
30 | | caovimo.idel |
. . . . . . . . . 10
 |
31 | 30 | a1i 9 |
. . . . . . . . 9
   |
32 | | id 19 |
. . . . . . . . 9
   |
33 | 29, 31, 32 | caovcomd 6027 |
. . . . . . . 8
           |
34 | | oveq1 5878 |
. . . . . . . . . 10
           |
35 | | id 19 |
. . . . . . . . . 10
   |
36 | 34, 35 | eqeq12d 2192 |
. . . . . . . . 9
     
       |
37 | 36, 20 | vtoclga 2803 |
. . . . . . . 8
       |
38 | 33, 37 | eqtrd 2210 |
. . . . . . 7
       |
39 | 38 | adantr 276 |
. . . . . 6
             |
40 | 39 | 3ad2ant3 1020 |
. . . . 5
  
                  |
41 | 3, 28, 40 | 3eqtr3d 2218 |
. . . 4
  
           
  |
42 | 41 | 3expib 1206 |
. . 3
                   |
43 | 42 | alrimivv 1875 |
. 2
                   
   |
44 | | eleq1 2240 |
. . . 4
 
   |
45 | | oveq2 5879 |
. . . . 5
           |
46 | 45 | eqeq1d 2186 |
. . . 4
     
       |
47 | 44, 46 | anbi12d 473 |
. . 3
                 |
48 | 47 | mo4 2087 |
. 2
        
                  
   |
49 | 43, 48 | sylibr 134 |
1
           |