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

  |
2 | | difeq2 3247 |
. . . 4

      |
3 | 1, 2 | uneq12d 3290 |
. . 3

    
     |
4 | 3 | eqeq2d 2189 |
. 2

    
       |
5 | | id 19 |
. . . 4
   |
6 | | difeq2 3247 |
. . . 4
       |
7 | 5, 6 | uneq12d 3290 |
. . 3
           |
8 | 7 | eqeq2d 2189 |
. 2
 
   
       |
9 | | id 19 |
. . . 4
           |
10 | | difeq2 3247 |
. . . 4
               |
11 | 9, 10 | uneq12d 3290 |
. . 3
                       |
12 | 11 | eqeq2d 2189 |
. 2
                         |
13 | | id 19 |
. . . 4
   |
14 | | difeq2 3247 |
. . . 4
       |
15 | 13, 14 | uneq12d 3290 |
. . 3
      
    |
16 | 15 | eqeq2d 2189 |
. 2
 
   

      |
17 | | un0 3456 |
. . . 4
   
   |
18 | | uncom 3279 |
. . . 4
   
     |
19 | | dif0 3493 |
. . . 4
   |
20 | 17, 18, 19 | 3eqtr3ri 2207 |
. . 3

    |
21 | 20 | a1i 9 |
. 2
   
DECID

      |
22 | | difundi 3387 |
. . . . . . 7
               |
23 | 22 | uneq2i 3286 |
. . . . . 6
                           |
24 | | undi 3383 |
. . . . . 6
       
                           |
25 | 23, 24 | eqtri 2198 |
. . . . 5
                                 |
26 | | uncom 3279 |
. . . . . . . . 9
         |
27 | 26 | uneq1i 3285 |
. . . . . . . 8
                 |
28 | | unass 3292 |
. . . . . . . 8
                 |
29 | 27, 28 | eqtri 2198 |
. . . . . . 7
                 |
30 | | simp3 999 |
. . . . . . . . . . . 12
   
DECID

  |
31 | 30 | ad3antrrr 492 |
. . . . . . . . . . 11
     

DECID

             |
32 | | simplrr 536 |
. . . . . . . . . . . 12
     

DECID

               |
33 | 32 | eldifad 3140 |
. . . . . . . . . . 11
     

DECID

             |
34 | 31, 33 | sseldd 3156 |
. . . . . . . . . 10
     

DECID

             |
35 | 34 | snssd 3736 |
. . . . . . . . 9
     

DECID

               |
36 | | ssequn1 3305 |
. . . . . . . . 9
         |
37 | 35, 36 | sylib 122 |
. . . . . . . 8
     

DECID

                 |
38 | | simpr 110 |
. . . . . . . . 9
     

DECID

          
      |
39 | 38 | uneq2d 3289 |
. . . . . . . 8
     

DECID

                         |
40 | 37, 39 | eqtr3d 2212 |
. . . . . . 7
     

DECID

          
          |
41 | 29, 40 | eqtr4id 2229 |
. . . . . 6
     

DECID

                     |
42 | | unass 3292 |
. . . . . . . 8
                     |
43 | | uncom 3279 |
. . . . . . . . . 10
                 |
44 | | simp1 997 |
. . . . . . . . . . . 12
   
DECID



DECID
  |
45 | 44 | ad3antrrr 492 |
. . . . . . . . . . 11
     

DECID

           

DECID   |
46 | | dcdifsnid 6499 |
. . . . . . . . . . 11
   
DECID
           |
47 | 45, 34, 46 | syl2anc 411 |
. . . . . . . . . 10
     

DECID

                     |
48 | 43, 47 | eqtrid 2222 |
. . . . . . . . 9
     

DECID

                     |
49 | 48 | uneq2d 3289 |
. . . . . . . 8
     

DECID

               
         |
50 | 42, 49 | eqtrid 2222 |
. . . . . . 7
     

DECID

                         |
51 | | simplrl 535 |
. . . . . . . . 9
     

DECID

          
  |
52 | 51, 31 | sstrd 3165 |
. . . . . . . 8
     

DECID

          
  |
53 | | ssequn1 3305 |
. . . . . . . 8

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

DECID

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

DECID

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

DECID

                                   |
57 | 25, 56 | eqtrid 2222 |
. . . 4
     

DECID

                           |
58 | | inidm 3344 |
. . . 4
   |
59 | 57, 58 | eqtr2di 2227 |
. . 3
     

DECID

          
              |
60 | 59 | ex 115 |
. 2
    

DECID

      
                   |
61 | | simp2 998 |
. 2
   
DECID

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


     |