Step | Hyp | Ref
| Expression |
1 | | constr3cycl.f |
. . . . . 6
                                      |
2 | | constr3cycl.p |
. . . . . 6
                     |
3 | 1, 2 | constr3trllem1 25457 |
. . . . 5
  USGrph
     
  
   Word   |
4 | | wrdf 12723 |
. . . . 5
 Word
   ..^      
  |
5 | 3, 4 | syl 17 |
. . . 4
  USGrph
     
  
      ..^         |
6 | 1, 2 | constr3lem2 25453 |
. . . . 5
     |
7 | | usgraf1o 25164 |
. . . . . . . . . . . 12
 USGrph       |
8 | | 3cycl3dv 25449 |
. . . . . . . . . . . . . 14
  USGrph
     
  
   
   |
9 | | usgraedgrnv 25183 |
. . . . . . . . . . . . . . . . . . . 20
  USGrph
   

   |
10 | 9 | ex 441 |
. . . . . . . . . . . . . . . . . . 19
 USGrph          |
11 | | usgraedgrnv 25183 |
. . . . . . . . . . . . . . . . . . . 20
  USGrph
   

   |
12 | 11 | ex 441 |
. . . . . . . . . . . . . . . . . . 19
 USGrph          |
13 | 10, 12 | anim12d 572 |
. . . . . . . . . . . . . . . . . 18
 USGrph       
     
     |
14 | 13 | com12 31 |
. . . . . . . . . . . . . . . . 17
    
     USGrph
 


     |
15 | 14 | 3adant2 1049 |
. . . . . . . . . . . . . . . 16
    
    
   USGrph
 


     |
16 | 15 | impcom 437 |
. . . . . . . . . . . . . . 15
  USGrph
     
  
      
    |
17 | 1, 2 | constr3lem5 25455 |
. . . . . . . . . . . . . . . . 17
                                       |
18 | 17 | jctl 550 |
. . . . . . . . . . . . . . . 16
     
 
   USGrph      
  
           
                                           


  
USGrph      
  
               |
19 | 18 | exp31 615 |
. . . . . . . . . . . . . . 15
     
 
 USGrph       
  
    

                                                


  
USGrph      
  
                 |
20 | 16, 19 | mpancom 682 |
. . . . . . . . . . . . . 14
  USGrph
     
  
                        
           
                 
 
   USGrph      
  
                 |
21 | 8, 20 | mpd 15 |
. . . . . . . . . . . . 13
  USGrph
     
  
                                                   


  
USGrph      
  
                |
22 | 21 | ex 441 |
. . . . . . . . . . . 12
 USGrph       
  
      
                                           


  
USGrph      
  
                 |
23 | 7, 22 | mpid 41 |
. . . . . . . . . . 11
 USGrph       
  
               
           
                 
 
   USGrph      
  
                |
24 | 23 | imp 436 |
. . . . . . . . . 10
  USGrph
     
  
                                              


  
USGrph      
  
               |
25 | 24 | adantl 473 |
. . . . . . . . 9
       USGrph    
    
   
                                           


  
USGrph      
  
               |
26 | | c0ex 9655 |
. . . . . . . . . . 11
 |
27 | | 1ex 9656 |
. . . . . . . . . . 11
 |
28 | | 2z 10993 |
. . . . . . . . . . 11
 |
29 | 26, 27, 28 | 3pm3.2i 1208 |
. . . . . . . . . 10
   |
30 | | eqidd 2472 |
. . . . . . . . . . . . . . 15
           |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . 14
                                            


  
USGrph      
  
                         |
32 | | f1of1 5827 |
. . . . . . . . . . . . . . . . . . 19
           |
33 | 32 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
     
 
   USGrph      
  
           
      |
34 | | 3simpa 1027 |
. . . . . . . . . . . . . . . . . . . 20
    
    
     
  
   |
35 | 34 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
  USGrph
     
  
         
   |
36 | 35 | ad3antlr 745 |
. . . . . . . . . . . . . . . . . 18
     
 
   USGrph      
  
           
  
  
    |
37 | | f1ocnvfvrneq 6202 |
. . . . . . . . . . . . . . . . . 18
     
  
  
                   
    
    |
38 | 33, 36, 37 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
     
 
   USGrph      
  
           
                
    
    |
39 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . . . 23
  


  
   |
40 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   |
41 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
   |
42 | 40, 41 | anim12i 576 |
. . . . . . . . . . . . . . . . . . . . . . 23
  


  
   |
43 | | preq12bg 4146 |
. . . . . . . . . . . . . . . . . . . . . . 23
  


     
 
          |
44 | 39, 42, 43 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . 22
  


     
 
          |
45 | | df-ne 2643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

  |
46 | | pm2.21 111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
47 | 45, 46 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   |
48 | 47 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
   |
49 | 48 | com12 31 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

   |
50 | 49 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  

   |
51 | | df-ne 2643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

  |
52 | | pm2.21 111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
53 | 51, 52 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
54 | 53 | 3ad2ant3 1053 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
   |
55 | 54 | com12 31 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  

   |
56 | 55 | eqcoms 2479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

   |
57 | 56 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  

   |
58 | 50, 57 | jaoi 386 |
. . . . . . . . . . . . . . . . . . . . . 22
        

   |
59 | 44, 58 | syl6bi 236 |
. . . . . . . . . . . . . . . . . . . . 21
  


     
 
  

    |
60 | 59 | com23 80 |
. . . . . . . . . . . . . . . . . . . 20
  


   

  
        |
61 | 60 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
     
 
 USGrph       
  
    

  
        |
62 | 61 | imp 436 |
. . . . . . . . . . . . . . . . . 18
      
 
 USGrph       
  
   
            |
63 | 62 | adantr 472 |
. . . . . . . . . . . . . . . . 17
     
 
   USGrph      
  
           
  
       |
64 | 38, 63 | syld 44 |
. . . . . . . . . . . . . . . 16
     
 
   USGrph      
  
           
                
   |
65 | 64 | adantl 473 |
. . . . . . . . . . . . . . 15
                                            


  
USGrph      
  
                                 |
66 | | eqeq12 2484 |
. . . . . . . . . . . . . . . . . 18
                                                       |
67 | 66 | 3adant3 1050 |
. . . . . . . . . . . . . . . . 17
                                                                   |
68 | 67 | imbi1d 324 |
. . . . . . . . . . . . . . . 16
                                                

                
    |
69 | 68 | adantr 472 |
. . . . . . . . . . . . . . 15
                                            


  
USGrph      
  
                                        
    |
70 | 65, 69 | mpbird 240 |
. . . . . . . . . . . . . 14
                                            


  
USGrph      
  
                         |
71 | | 3simpb 1028 |
. . . . . . . . . . . . . . . . . . . 20
    
    
     
  
   |
72 | 71 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
  USGrph
     
  
         
   |
73 | 72 | ad3antlr 745 |
. . . . . . . . . . . . . . . . . 18
     
 
   USGrph      
  
           
  
  
    |
74 | | f1ocnvfvrneq 6202 |
. . . . . . . . . . . . . . . . . 18
     
  
  
                   
    
    |
75 | 33, 73, 74 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
     
 
   USGrph      
  
           
                
    
    |
76 | | preq12bg 4146 |
. . . . . . . . . . . . . . . . . . . . . 22
  


     
 
          |
77 | | pm2.21 111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
78 | 45, 77 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
79 | 78 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
   |
80 | 79 | com12 31 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  

   |
81 | 80 | eqcoms 2479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

   |
82 | 81 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  

   |
83 | | df-ne 2643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

  |
84 | | pm2.21 111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
85 | 83, 84 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   |
86 | 85 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
   |
87 | 86 | com12 31 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

   |
88 | 87 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  

   |
89 | 82, 88 | jaoi 386 |
. . . . . . . . . . . . . . . . . . . . . 22
        

   |
90 | 76, 89 | syl6bi 236 |
. . . . . . . . . . . . . . . . . . . . 21
  


     
 
  

    |
91 | 90 | com23 80 |
. . . . . . . . . . . . . . . . . . . 20
  


   

  
        |
92 | 91 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
     
 
 USGrph       
  
    

  
        |
93 | 92 | imp 436 |
. . . . . . . . . . . . . . . . . 18
      
 
 USGrph       
  
   
            |
94 | 93 | adantr 472 |
. . . . . . . . . . . . . . . . 17
     
 
   USGrph      
  
           
  
       |
95 | 75, 94 | syld 44 |
. . . . . . . . . . . . . . . 16
     
 
   USGrph      
  
           
                
   |
96 | 95 | adantl 473 |
. . . . . . . . . . . . . . 15
                                            


  
USGrph      
  
                                 |
97 | | eqeq12 2484 |
. . . . . . . . . . . . . . . . . 18
                                                       |
98 | 97 | 3adant2 1049 |
. . . . . . . . . . . . . . . . 17
                                                                   |
99 | 98 | imbi1d 324 |
. . . . . . . . . . . . . . . 16
                                                

                
    |
100 | 99 | adantr 472 |
. . . . . . . . . . . . . . 15
                                            


  
USGrph      
  
                                        
    |
101 | 96, 100 | mpbird 240 |
. . . . . . . . . . . . . 14
                                            


  
USGrph      
  
                         |
102 | 31, 70, 101 | 3jca 1210 |
. . . . . . . . . . . . 13
                                            


  
USGrph      
  
                                               |
103 | 102 | adantl 473 |
. . . . . . . . . . . 12
  
              
           
                 
 
   USGrph      
  
                       
                   
    |
104 | | fveq2 5879 |
. . . . . . . . . . . . . . . 16
           |
105 | 104 | eqeq2d 2481 |
. . . . . . . . . . . . . . 15
         
           |
106 | | eqeq2 2482 |
. . . . . . . . . . . . . . 15
 
   |
107 | 105, 106 | imbi12d 327 |
. . . . . . . . . . . . . 14
                    
    |
108 | | fveq2 5879 |
. . . . . . . . . . . . . . . 16
           |
109 | 108 | eqeq2d 2481 |
. . . . . . . . . . . . . . 15
         
           |
110 | | eqeq2 2482 |
. . . . . . . . . . . . . . 15
 
   |
111 | 109, 110 | imbi12d 327 |
. . . . . . . . . . . . . 14
                    
    |
112 | | fveq2 5879 |
. . . . . . . . . . . . . . . 16
           |
113 | 112 | eqeq2d 2481 |
. . . . . . . . . . . . . . 15
         
           |
114 | | eqeq2 2482 |
. . . . . . . . . . . . . . 15
 
   |
115 | 113, 114 | imbi12d 327 |
. . . . . . . . . . . . . 14
                    
    |
116 | 107, 111,
115 | raltpg 4014 |
. . . . . . . . . . . . 13
 
  
            

                   
               |
117 | 116 | adantr 472 |
. . . . . . . . . . . 12
  
              
           
                 
 
   USGrph      
  
                                       
                   
     |
118 | 103, 117 | mpbird 240 |
. . . . . . . . . . 11
  
              
           
                 
 
   USGrph      
  
              
            
   |
119 | | pm3.22 456 |
. . . . . . . . . . . . . . . . . . . . 21
    
       
  
   |
120 | 119 | 3adant3 1050 |
. . . . . . . . . . . . . . . . . . . 20
    
    
     
  
   |
121 | 120 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
  USGrph
     
  
         
   |
122 | 121 | ad3antlr 745 |
. . . . . . . . . . . . . . . . . 18
     
 
   USGrph      
  
           
  
  
    |
123 | | f1ocnvfvrneq 6202 |
. . . . . . . . . . . . . . . . . 18
     
  
  
                   
    
    |
124 | 33, 122, 123 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
     
 
   USGrph      
  
           
                
    
    |
125 | | preq12bg 4146 |
. . . . . . . . . . . . . . . . . . . . . . 23
  


     
 
          |
126 | 42, 39, 125 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . 22
  


     
 
          |
127 | | pm2.21 111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
128 | 45, 127 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
129 | 128 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
   |
130 | 129 | com12 31 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  

   |
131 | 130 | eqcoms 2479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

   |
132 | 131 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  

   |
133 | | pm2.21 111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
134 | 51, 133 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   |
135 | 134 | 3ad2ant3 1053 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
   |
136 | 135 | com12 31 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

   |
137 | 136 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  

   |
138 | 132, 137 | jaoi 386 |
. . . . . . . . . . . . . . . . . . . . . 22
        

   |
139 | 126, 138 | syl6bi 236 |
. . . . . . . . . . . . . . . . . . . . 21
  


     
 
  

    |
140 | 139 | com23 80 |
. . . . . . . . . . . . . . . . . . . 20
  


   

  
        |
141 | 140 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
     
 
 USGrph       
  
    

  
        |
142 | 141 | imp 436 |
. . . . . . . . . . . . . . . . . 18
      
 
 USGrph       
  
   
            |
143 | 142 | adantr 472 |
. . . . . . . . . . . . . . . . 17
     
 
   USGrph      
  
           
  
       |
144 | 124, 143 | syld 44 |
. . . . . . . . . . . . . . . 16
     
 
   USGrph      
  
           
                
   |
145 | 144 | adantl 473 |
. . . . . . . . . . . . . . 15
                                            


  
USGrph      
  
                                 |
146 | | eqeq12 2484 |
. . . . . . . . . . . . . . . . . . 19
                                                       |
147 | 146 | ancoms 460 |
. . . . . . . . . . . . . . . . . 18
                                                       |
148 | 147 | 3adant3 1050 |
. . . . . . . . . . . . . . . . 17
                                                                   |
149 | 148 | imbi1d 324 |
. . . . . . . . . . . . . . . 16
                                                

                
    |
150 | 149 | adantr 472 |
. . . . . . . . . . . . . . 15
                                            


  
USGrph      
  
                                        
    |
151 | 145, 150 | mpbird 240 |
. . . . . . . . . . . . . 14
                                            


  
USGrph      
  
                         |
152 | | eqidd 2472 |
. . . . . . . . . . . . . . 15
           |
153 | 152 | a1i 11 |
. . . . . . . . . . . . . 14
                                            


  
USGrph      
  
                         |
154 | | 3simpc 1029 |
. . . . . . . . . . . . . . . . . . . 20
    
    
     
  
   |
155 | 154 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
  USGrph
     
  
         
   |
156 | 155 | ad3antlr 745 |
. . . . . . . . . . . . . . . . . 18
     
 
   USGrph      
  
           
  
  
    |
157 | | f1ocnvfvrneq 6202 |
. . . . . . . . . . . . . . . . . 18
     
  
  
                   
    
    |
158 | 33, 156, 157 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
     
 
   USGrph      
  
           
                
    
    |
159 | | preq12bg 4146 |
. . . . . . . . . . . . . . . . . . . . . . 23
  


     
 
          |
160 | 42, 159 | sylancom 680 |
. . . . . . . . . . . . . . . . . . . . . 22
  


     
 
          |
161 | | pm2.21 111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
162 | 83, 161 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   |
163 | 162 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
   |
164 | 163 | com12 31 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

   |
165 | 164 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  

   |
166 | | pm2.21 111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
167 | 45, 166 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
168 | 167 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
   |
169 | 168 | com12 31 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  

   |
170 | 169 | eqcoms 2479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

   |
171 | 170 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  

   |
172 | 165, 171 | jaoi 386 |
. . . . . . . . . . . . . . . . . . . . . 22
        

   |
173 | 160, 172 | syl6bi 236 |
. . . . . . . . . . . . . . . . . . . . 21
  


     
 
  

    |
174 | 173 | com23 80 |
. . . . . . . . . . . . . . . . . . . 20
  


   

  
        |
175 | 174 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
     
 
 USGrph       
  
    

  
        |
176 | 175 | imp 436 |
. . . . . . . . . . . . . . . . . 18
      
 
 USGrph       
  
   
            |
177 | 176 | adantr 472 |
. . . . . . . . . . . . . . . . 17
     
 
   USGrph      
  
           
  
       |
178 | 158, 177 | syld 44 |
. . . . . . . . . . . . . . . 16
     
 
   USGrph      
  
           
                
   |
179 | 178 | adantl 473 |
. . . . . . . . . . . . . . 15
                                            


  
USGrph      
  
                                 |
180 | | eqeq12 2484 |
. . . . . . . . . . . . . . . . . 18
                                                       |
181 | 180 | 3adant1 1048 |
. . . . . . . . . . . . . . . . 17
                                                                   |
182 | 181 | imbi1d 324 |
. . . . . . . . . . . . . . . 16
                                                

                
    |
183 | 182 | adantr 472 |
. . . . . . . . . . . . . . 15
                                            


  
USGrph      
  
                                        
    |
184 | 179, 183 | mpbird 240 |
. . . . . . . . . . . . . 14
                                            


  
USGrph      
  
                         |
185 | 151, 153,
184 | 3jca 1210 |
. . . . . . . . . . . . 13
                                            


  
USGrph      
  
                                               |
186 | 185 | adantl 473 |
. . . . . . . . . . . 12
  
              
           
                 
 
   USGrph      
  
                       
                   
    |
187 | 104 | eqeq2d 2481 |
. . . . . . . . . . . . . . 15
         
           |
188 | | eqeq2 2482 |
. . . . . . . . . . . . . . 15
 
   |
189 | 187, 188 | imbi12d 327 |
. . . . . . . . . . . . . 14
                    
    |
190 | 108 | eqeq2d 2481 |
. . . . . . . . . . . . . . 15
         
           |
191 | | eqeq2 2482 |
. . . . . . . . . . . . . . 15
 
   |
192 | 190, 191 | imbi12d 327 |
. . . . . . . . . . . . . 14
                    
    |
193 | 112 | eqeq2d 2481 |
. . . . . . . . . . . . . . 15
         
           |
194 | | eqeq2 2482 |
. . . . . . . . . . . . . . 15
 
   |
195 | 193, 194 | imbi12d 327 |
. . . . . . . . . . . . . 14
                    
    |
196 | 189, 192,
195 | raltpg 4014 |
. . . . . . . . . . . . 13
 
  
            

                   
               |
197 | 196 | adantr 472 |
. . . . . . . . . . . 12
  
              
           
                 
 
   USGrph      
  
                                       
                   
     |
198 | 186, 197 | mpbird 240 |
. . . . . . . . . . 11
  
              
           
                 
 
   USGrph      
  
              
            
   |
199 | | pm3.22 456 |
. . . . . . . . . . . . . . . . . . . . 21
    
       
  
   |
200 | 199 | 3adant2 1049 |
. . . . . . . . . . . . . . . . . . . 20
    
    
     
  
   |
201 | 200 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
  USGrph
     
  
         
   |
202 | 201 | ad3antlr 745 |
. . . . . . . . . . . . . . . . . 18
     
 
   USGrph      
  
           
  
  
    |
203 | | f1ocnvfvrneq 6202 |
. . . . . . . . . . . . . . . . . 18
     
  
  
                   
    
    |
204 | 33, 202, 203 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
     
 
   USGrph      
  
           
                
    
    |
205 | | preq12bg 4146 |
. . . . . . . . . . . . . . . . . . . . . . 23
  


     
 
          |
206 | 205 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . 22
  


     
 
          |
207 | | pm2.21 111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
208 | 45, 207 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   |
209 | 208 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
   |
210 | 209 | com12 31 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

   |
211 | 210 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  

   |
212 | | pm2.21 111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
213 | 83, 212 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
214 | 213 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
   |
215 | 214 | com12 31 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  

   |
216 | 215 | eqcoms 2479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  

   |
217 | 216 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  

   |
218 | 211, 217 | jaoi 386 |
. . . . . . . . . . . . . . . . . . . . . 22
        

   |
219 | 206, 218 | syl6bi 236 |
. . . . . . . . . . . . . . . . . . . . 21
  


     
 
  

    |
220 | 219 | com23 80 |
. . . . . . . . . . . . . . . . . . . 20
  


   

  
        |
221 | 220 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
     
 
 USGrph       
  
    

  
        |
222 | 221 | imp 436 |
. . . . . . . . . . . . . . . . . 18
      
 
 USGrph       
  
   
            |
223 | 222 | adantr 472 |
. . . . . . . . . . . . . . . . 17
     
 
   USGrph      
  
           
  
       |
224 | 204, 223 | syld 44 |
. . . . . . . . . . . . . . . 16
     
 
   USGrph      
  
           
                
   |
225 | 224 | adantl 473 |
. . . . . . . . . . . . . . 15
                                            


  
USGrph      
  
                                 |
226 | | eqeq12 2484 |
. . . . . . . . . . . . . . . . . . 19
                                                       |
227 | 226 | ancoms 460 |
. . . . . . . . . . . . . . . . . 18
                                                       |
228 | 227 | 3adant2 1049 |
. . . . . . . . . . . . . . . . 17
                                                                   |
229 | 228 | imbi1d 324 |
. . . . . . . . . . . . . . . 16
                                                

                
    |
230 | 229 | adantr 472 |
. . . . . . . . . . . . . . 15
                                            


  
USGrph      
  
                                        
    |
231 | 225, 230 | mpbird 240 |
. . . . . . . . . . . . . 14
                                            


  
USGrph      
  
                         |
232 | | pm3.22 456 |
. . . . . . . . . . . . . . . . . . . . 21
    
       
  
   |
233 | 232 | 3adant1 1048 |
. . . . . . . . . . . . . . . . . . . 20
    
    
     
  
   |
234 | 233 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
  USGrph
     
  
         
   |
235 | 234 | ad3antlr 745 |
. . . . . . . . . . . . . . . . . 18
     
 
   USGrph      
  
           
  
  
    |
236 | | f1ocnvfvrneq 6202 |
. . . . . . . . . . . . . . . . . 18
     
    |