Step | Hyp | Ref
| Expression |
1 | | simp13 989 |
. . . . . . 7
   
   |
2 | | cvllat 29813 |
. . . . . . 7

  |
3 | 1, 2 | syl 16 |
. . . . . 6
   
   |
4 | | simp2 958 |
. . . . . 6
   
   |
5 | | cvlcvr1.b |
. . . . . . . 8
     |
6 | | cvlcvr1.a |
. . . . . . . 8
     |
7 | 5, 6 | atbase 29776 |
. . . . . . 7
   |
8 | 7 | 3ad2ant3 980 |
. . . . . 6
   
   |
9 | | cvlcvr1.l |
. . . . . . 7
     |
10 | | eqid 2408 |
. . . . . . 7
         |
11 | | cvlcvr1.j |
. . . . . . 7
     |
12 | 5, 9, 10, 11 | latnle 14473 |
. . . . . 6
 
             |
13 | 3, 4, 8, 12 | syl3anc 1184 |
. . . . 5
   
 
           |
14 | 13 | biimpd 199 |
. . . 4
   
 
           |
15 | | simpl13 1034 |
. . . . . . . . 9
   

                  |
16 | 15, 2 | syl 16 |
. . . . . . . 8
   

                  |
17 | | simprll 739 |
. . . . . . . 8
   

                  |
18 | | simpl2 961 |
. . . . . . . . 9
   

                  |
19 | | simpl3 962 |
. . . . . . . . . 10
   

                  |
20 | 19, 7 | syl 16 |
. . . . . . . . 9
   

                  |
21 | 5, 11 | latjcl 14438 |
. . . . . . . . 9
 
     |
22 | 16, 18, 20, 21 | syl3anc 1184 |
. . . . . . . 8
   

                    |
23 | | simprrr 742 |
. . . . . . . 8
   

                    |
24 | | simprrl 741 |
. . . . . . . . . 10
   

                        |
25 | | simpl11 1032 |
. . . . . . . . . . 11
   

                  |
26 | | simpl12 1033 |
. . . . . . . . . . 11
   

                  |
27 | | cvlatl 29812 |
. . . . . . . . . . . 12

  |
28 | 15, 27 | syl 16 |
. . . . . . . . . . 11
   

                  |
29 | 5, 9, 10, 6 | atlrelat1 29808 |
. . . . . . . . . . 11
   
        

    |
30 | 25, 26, 28, 18, 17, 29 | syl311anc 1198 |
. . . . . . . . . 10
   

                      

     |
31 | 24, 30 | mpd 15 |
. . . . . . . . 9
   

                 
   |
32 | 16 | adantr 452 |
. . . . . . . . . . . . 13
    


 
        
           |
33 | 5, 6 | atbase 29776 |
. . . . . . . . . . . . . 14
   |
34 | 33 | ad2antrl 709 |
. . . . . . . . . . . . 13
    


 
        
           |
35 | 17 | adantr 452 |
. . . . . . . . . . . . 13
    


 
        
           |
36 | 22 | adantr 452 |
. . . . . . . . . . . . 13
    


 
        
             |
37 | | simprrr 742 |
. . . . . . . . . . . . 13
    


 
        
           |
38 | 23 | adantr 452 |
. . . . . . . . . . . . 13
    


 
        
             |
39 | 5, 9, 32, 34, 35, 36, 37, 38 | lattrd 14446 |
. . . . . . . . . . . 12
    


 
        
             |
40 | 15 | adantr 452 |
. . . . . . . . . . . . 13
    


 
        
           |
41 | | simprl 733 |
. . . . . . . . . . . . 13
    


 
        
           |
42 | | simpll3 998 |
. . . . . . . . . . . . 13
    


 
        
           |
43 | | simpll2 997 |
. . . . . . . . . . . . 13
    


 
        
           |
44 | | simprrl 741 |
. . . . . . . . . . . . 13
    


 
        
           |
45 | 5, 9, 11, 6 | cvlexch1 29815 |
. . . . . . . . . . . . 13
  
   
      |
46 | 40, 41, 42, 43, 44, 45 | syl131anc 1197 |
. . . . . . . . . . . 12
    


 
        
           
     |
47 | 39, 46 | mpd 15 |
. . . . . . . . . . 11
    


 
        
             |
48 | | simprlr 740 |
. . . . . . . . . . . . 13
   

               
  |
49 | 48 | adantr 452 |
. . . . . . . . . . . 12
    


 
        
           |
50 | 5, 9, 11, 6 | cvlexchb1 29817 |
. . . . . . . . . . . 12
  
            |
51 | 40, 42, 41, 43, 49, 50 | syl131anc 1197 |
. . . . . . . . . . 11
    


 
        
           
       |
52 | 47, 51 | mpbid 202 |
. . . . . . . . . 10
    


 
        
               |
53 | 9, 10 | pltle 14377 |
. . . . . . . . . . . . . 14
 
           |
54 | 25, 18, 17, 53 | syl3anc 1184 |
. . . . . . . . . . . . 13
   

                      
   |
55 | 24, 54 | mpd 15 |
. . . . . . . . . . . 12
   

                  |
56 | 55 | adantr 452 |
. . . . . . . . . . 11
    


 
        
           |
57 | 5, 9, 11 | latjle12 14450 |
. . . . . . . . . . . 12
  
    
     |
58 | 32, 43, 34, 35, 57 | syl13anc 1186 |
. . . . . . . . . . 11
    


 
        
           
     |
59 | 56, 37, 58 | mpbi2and 888 |
. . . . . . . . . 10
    


 
        
             |
60 | 52, 59 | eqbrtrd 4196 |
. . . . . . . . 9
    


 
        
             |
61 | 31, 60 | rexlimddv 2798 |
. . . . . . . 8
   

                 
  |
62 | 5, 9, 16, 17, 22, 23, 61 | latasymd 14445 |
. . . . . . 7
   

                    |
63 | 62 | exp44 597 |
. . . . . 6
   
                     |
64 | 63 | imp 419 |
. . . . 5
   



                  |
65 | 64 | ralrimdva 2760 |
. . . 4
   
 

        
 

     |
66 | 14, 65 | jcad 520 |
. . 3
   
 
                            |
67 | 3, 4, 8, 21 | syl3anc 1184 |
. . . 4
   
     |
68 | | cvlcvr1.c |
. . . . 5
   |
69 | 5, 9, 10, 68 | cvrval2 29761 |
. . . 4
 

                                   |
70 | 3, 4, 67, 69 | syl3anc 1184 |
. . 3
   
              

                  |
71 | 66, 70 | sylibrd 226 |
. 2
   
 
       |
72 | 3 | adantr 452 |
. . . . 5
   

        |
73 | | simpl2 961 |
. . . . 5
   

        |
74 | 67 | adantr 452 |
. . . . 5
   

          |
75 | | simpr 448 |
. . . . 5
   

            |
76 | 5, 10, 68 | cvrlt 29757 |
. . . . 5
   
                 |
77 | 72, 73, 74, 75, 76 | syl31anc 1187 |
. . . 4
   

                |
78 | 77 | ex 424 |
. . 3
   
     
           |
79 | 78, 13 | sylibrd 226 |
. 2
   
     
   |
80 | 71, 79 | impbid 184 |
1
   
 
       |