Step | Hyp | Ref
| Expression |
1 | | sseq1 3465 |
. . . . . 6

 
    |
2 | | sseq1 3465 |
. . . . . . 7


   |
3 | 2 | rexbidv 2913 |
. . . . . 6

 

   |
4 | 1, 3 | imbi12d 326 |
. . . . 5

 
 

       |
5 | 4 | imbi2d 322 |
. . . 4

   [ ] 
  
 
 
[ ] 
        |
6 | | sseq1 3465 |
. . . . . 6
 

    |
7 | | sseq1 3465 |
. . . . . . 7
 
   |
8 | 7 | rexbidv 2913 |
. . . . . 6
  

   |
9 | 6, 8 | imbi12d 326 |
. . . . 5
     
  
    |
10 | 9 | imbi2d 322 |
. . . 4
    [ ]

  
 
 
[ ] 
  
     |
11 | | sseq1 3465 |
. . . . . 6
               |
12 | | sseq1 3465 |
. . . . . . 7
             |
13 | 12 | rexbidv 2913 |
. . . . . 6
      
        |
14 | 11, 13 | imbi12d 326 |
. . . . 5
        

               |
15 | 14 | imbi2d 322 |
. . . 4
        [ ] 
  
 
 
[ ] 
                |
16 | | sseq1 3465 |
. . . . . 6
 

    |
17 | | sseq1 3465 |
. . . . . . 7
 
   |
18 | 17 | rexbidv 2913 |
. . . . . 6
  

   |
19 | 16, 18 | imbi12d 326 |
. . . . 5
     
  
    |
20 | 19 | imbi2d 322 |
. . . 4
    [ ]

  
 
 
[ ] 
  
     |
21 | | 0ss 3775 |
. . . . . . . 8
 |
22 | 21 | rgenw 2761 |
. . . . . . 7

 |
23 | | r19.2z 3870 |
. . . . . . 7
  


  |
24 | 22, 23 | mpan2 682 |
. . . . . 6


  |
25 | 24 | adantr 471 |
. . . . 5
  [ ] 

  |
26 | 25 | a1d 26 |
. . . 4
  [ ] 
      |
27 | | id 22 |
. . . . . . . . 9
             |
28 | 27 | unssad 3623 |
. . . . . . . 8
     
   |
29 | 28 | imim1i 60 |
. . . . . . 7
 
 
       
   |
30 | | sseq2 3466 |
. . . . . . . . . . 11
 
   |
31 | 30 | cbvrexv 3032 |
. . . . . . . . . 10
 

  |
32 | | simpr 467 |
. . . . . . . . . . . . . 14
   [ ] 
             |
33 | 32 | unssbd 3624 |
. . . . . . . . . . . . 13
   [ ] 
           |
34 | | vex 3060 |
. . . . . . . . . . . . . 14
 |
35 | 34 | snss 4109 |
. . . . . . . . . . . . 13
 
     |
36 | 33, 35 | sylibr 217 |
. . . . . . . . . . . 12
   [ ] 
         |
37 | | eluni2 4216 |
. . . . . . . . . . . 12
 

  |
38 | 36, 37 | sylib 201 |
. . . . . . . . . . 11
   [ ] 
      
  |
39 | | reeanv 2970 |
. . . . . . . . . . . 12
  
 
 

   |
40 | | simpllr 774 |
. . . . . . . . . . . . . . . 16
    [ ]

            
[ ]   |
41 | | simprlr 778 |
. . . . . . . . . . . . . . . 16
    [ ]

            
  |
42 | | simprll 777 |
. . . . . . . . . . . . . . . 16
    [ ]

            
  |
43 | | sorpssun 6610 |
. . . . . . . . . . . . . . . 16
 [ ] 
 
    |
44 | 40, 41, 42, 43 | syl12anc 1274 |
. . . . . . . . . . . . . . 15
    [ ]

            
    |
45 | | simprrr 780 |
. . . . . . . . . . . . . . . 16
    [ ]

            
  |
46 | | simprrl 779 |
. . . . . . . . . . . . . . . . 17
    [ ]

            
  |
47 | 46 | snssd 4130 |
. . . . . . . . . . . . . . . 16
    [ ]

            
    |
48 | | unss12 3618 |
. . . . . . . . . . . . . . . 16
 
  
        |
49 | 45, 47, 48 | syl2anc 671 |
. . . . . . . . . . . . . . 15
    [ ]

            
        |
50 | | sseq2 3466 |
. . . . . . . . . . . . . . . 16
            
    |
51 | 50 | rspcev 3162 |
. . . . . . . . . . . . . . 15
        
  
      |
52 | 44, 49, 51 | syl2anc 671 |
. . . . . . . . . . . . . 14
    [ ]

            

      |
53 | 52 | expr 624 |
. . . . . . . . . . . . 13
    [ ]

      
   
         |
54 | 53 | rexlimdvva 2898 |
. . . . . . . . . . . 12
   [ ] 
           
       |
55 | 39, 54 | syl5bir 226 |
. . . . . . . . . . 11
   [ ] 
        
 

       |
56 | 38, 55 | mpand 686 |
. . . . . . . . . 10
   [ ] 
                |
57 | 31, 56 | syl5bi 225 |
. . . . . . . . 9
   [ ] 
                |
58 | 57 | ex 440 |
. . . . . . . 8
  [ ] 
                 |
59 | 58 | a2d 29 |
. . . . . . 7
  [ ] 
      

      

        |
60 | 29, 59 | syl5 33 |
. . . . . 6
  [ ] 
 
 
       
        |
61 | 60 | a2i 14 |
. . . . 5
   [ ] 
  
    [ ]

               |
62 | 61 | a1i 11 |
. . . 4
    [ ]

  
    [ ]

                |
63 | 5, 10, 15, 20, 26, 62 | findcard2 7842 |
. . 3
   [ ] 
  
    |
64 | 63 | com12 32 |
. 2
  [ ] 

  
    |
65 | 64 | imp32 439 |
1
   [ ] 
    
  |