Step | Hyp | Ref
| Expression |
1 | | id 19 |
. . . 4

  |
2 | | difeq2 3113 |
. . . 4

      |
3 | 1, 2 | uneq12d 3156 |
. . 3

    
     |
4 | 3 | eqeq2d 2100 |
. 2

    
       |
5 | | id 19 |
. . . 4
   |
6 | | difeq2 3113 |
. . . 4
       |
7 | 5, 6 | uneq12d 3156 |
. . 3
           |
8 | 7 | eqeq2d 2100 |
. 2
 
   
       |
9 | | id 19 |
. . . 4
           |
10 | | difeq2 3113 |
. . . 4
               |
11 | 9, 10 | uneq12d 3156 |
. . 3
                       |
12 | 11 | eqeq2d 2100 |
. 2
                         |
13 | | id 19 |
. . . 4
   |
14 | | difeq2 3113 |
. . . 4
       |
15 | 13, 14 | uneq12d 3156 |
. . 3
      
    |
16 | 15 | eqeq2d 2100 |
. 2
 
   

      |
17 | | un0 3320 |
. . . 4
   
   |
18 | | uncom 3145 |
. . . 4
   
     |
19 | | dif0 3357 |
. . . 4
   |
20 | 17, 18, 19 | 3eqtr3ri 2118 |
. . 3

    |
21 | 20 | a1i 9 |
. 2
   
DECID

      |
22 | | difundi 3252 |
. . . . . . 7
               |
23 | 22 | uneq2i 3152 |
. . . . . 6
                           |
24 | | undi 3248 |
. . . . . 6
       
                           |
25 | 23, 24 | eqtri 2109 |
. . . . 5
                                 |
26 | | simp3 946 |
. . . . . . . . . . . 12
   
DECID

  |
27 | 26 | ad3antrrr 477 |
. . . . . . . . . . 11
     

DECID

             |
28 | | simplrr 504 |
. . . . . . . . . . . 12
     

DECID

               |
29 | 28 | eldifad 3011 |
. . . . . . . . . . 11
     

DECID

             |
30 | 27, 29 | sseldd 3027 |
. . . . . . . . . 10
     

DECID

             |
31 | 30 | snssd 3588 |
. . . . . . . . 9
     

DECID

               |
32 | | ssequn1 3171 |
. . . . . . . . 9
         |
33 | 31, 32 | sylib 121 |
. . . . . . . 8
     

DECID

                 |
34 | | simpr 109 |
. . . . . . . . 9
     

DECID

          
      |
35 | 34 | uneq2d 3155 |
. . . . . . . 8
     

DECID

                         |
36 | 33, 35 | eqtr3d 2123 |
. . . . . . 7
     

DECID

          
          |
37 | | uncom 3145 |
. . . . . . . . 9
         |
38 | 37 | uneq1i 3151 |
. . . . . . . 8
                 |
39 | | unass 3158 |
. . . . . . . 8
                 |
40 | 38, 39 | eqtri 2109 |
. . . . . . 7
                 |
41 | 36, 40 | syl6reqr 2140 |
. . . . . 6
     

DECID

                     |
42 | | unass 3158 |
. . . . . . . 8
                     |
43 | | uncom 3145 |
. . . . . . . . . 10
                 |
44 | | simp1 944 |
. . . . . . . . . . . 12
   
DECID



DECID
  |
45 | 44 | ad3antrrr 477 |
. . . . . . . . . . 11
     

DECID

           

DECID   |
46 | | dcdifsnid 6277 |
. . . . . . . . . . 11
   
DECID
           |
47 | 45, 30, 46 | syl2anc 404 |
. . . . . . . . . 10
     

DECID

                     |
48 | 43, 47 | syl5eq 2133 |
. . . . . . . . 9
     

DECID

                     |
49 | 48 | uneq2d 3155 |
. . . . . . . 8
     

DECID

               
         |
50 | 42, 49 | syl5eq 2133 |
. . . . . . 7
     

DECID

                         |
51 | | simplrl 503 |
. . . . . . . . 9
     

DECID

          
  |
52 | 51, 27 | sstrd 3036 |
. . . . . . . 8
     

DECID

          
  |
53 | | ssequn1 3171 |
. . . . . . . 8

    |
54 | 52, 53 | sylib 121 |
. . . . . . 7
     

DECID

               |
55 | 50, 54 | eqtrd 2121 |
. . . . . 6
     

DECID

                       |
56 | 41, 55 | ineq12d 3203 |
. . . . 5
     

DECID

                                   |
57 | 25, 56 | syl5eq 2133 |
. . . 4
     

DECID

                           |
58 | | inidm 3210 |
. . . 4
   |
59 | 57, 58 | syl6req 2138 |
. . 3
     

DECID

          
              |
60 | 59 | ex 114 |
. 2
    

DECID

      
                   |
61 | | simp2 945 |
. 2
   
DECID

  |
62 | 4, 8, 12, 16, 21, 60, 61 | findcard2sd 6662 |
1
   
DECID


     |