Step | Hyp | Ref
| Expression |
1 | | sconpcon 29962 |
. . 3
 SCon PCon |
2 | | sconpcon 29962 |
. . 3
 SCon PCon |
3 | | txpcon 29967 |
. . 3
  PCon PCon
  PCon |
4 | 1, 2, 3 | syl2an 480 |
. 2
  SCon SCon
  PCon |
5 | | simpll 761 |
. . . . . . . . 9
   SCon
SCon               
SCon |
6 | | simprl 765 |
. . . . . . . . . 10
   SCon
SCon               

     |
7 | | scontop 29963 |
. . . . . . . . . . . . 13
 SCon   |
8 | 7 | ad2antrr 733 |
. . . . . . . . . . . 12
   SCon
SCon               
  |
9 | | eqid 2453 |
. . . . . . . . . . . . 13
   |
10 | 9 | toptopon 19960 |
. . . . . . . . . . . 12

TopOn     |
11 | 8, 10 | sylib 200 |
. . . . . . . . . . 11
   SCon
SCon               
TopOn     |
12 | | scontop 29963 |
. . . . . . . . . . . . 13
 SCon   |
13 | 12 | ad2antlr 734 |
. . . . . . . . . . . 12
   SCon
SCon               
  |
14 | | eqid 2453 |
. . . . . . . . . . . . 13
   |
15 | 14 | toptopon 19960 |
. . . . . . . . . . . 12

TopOn     |
16 | 13, 15 | sylib 200 |
. . . . . . . . . . 11
   SCon
SCon               
TopOn     |
17 | | tx1cn 20636 |
. . . . . . . . . . 11
  TopOn   TopOn   
            |
18 | 11, 16, 17 | syl2anc 667 |
. . . . . . . . . 10
   SCon
SCon               
            |
19 | | cnco 20294 |
. . . . . . . . . 10
      
                      |
20 | 6, 18, 19 | syl2anc 667 |
. . . . . . . . 9
   SCon
SCon               
            |
21 | | simprr 767 |
. . . . . . . . . . 11
   SCon
SCon               
          |
22 | 21 | fveq2d 5874 |
. . . . . . . . . 10
   SCon
SCon               
                 
            |
23 | | iitopon 21923 |
. . . . . . . . . . . . 13
TopOn   ![[,] [,]](_icc.gif)    |
24 | 23 | a1i 11 |
. . . . . . . . . . . 12
   SCon
SCon               
TopOn   ![[,] [,]](_icc.gif)     |
25 | | txtopon 20618 |
. . . . . . . . . . . . 13
  TopOn   TopOn   
  TopOn        |
26 | 11, 16, 25 | syl2anc 667 |
. . . . . . . . . . . 12
   SCon
SCon               
  TopOn        |
27 | | cnf2 20277 |
. . . . . . . . . . . 12
  TopOn   ![[,] [,]](_icc.gif)     TopOn          
    ![[,] [,]](_icc.gif)          |
28 | 24, 26, 6, 27 | syl3anc 1269 |
. . . . . . . . . . 11
   SCon
SCon               
    ![[,] [,]](_icc.gif)          |
29 | | 0elunit 11757 |
. . . . . . . . . . 11
  ![[,] [,]](_icc.gif)   |
30 | | fvco3 5947 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       
                       |
31 | 28, 29, 30 | sylancl 669 |
. . . . . . . . . 10
   SCon
SCon               
  
            
            |
32 | | 1elunit 11758 |
. . . . . . . . . . 11
  ![[,] [,]](_icc.gif)   |
33 | | fvco3 5947 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       
                       |
34 | 28, 32, 33 | sylancl 669 |
. . . . . . . . . 10
   SCon
SCon               
  
            
            |
35 | 22, 31, 34 | 3eqtr4d 2497 |
. . . . . . . . 9
   SCon
SCon               
  
                       |
36 | | sconpht 29964 |
. . . . . . . . 9
  SCon  
            
         
                         ![[,] [,]](_icc.gif)       
           |
37 | 5, 20, 35, 36 | syl3anc 1269 |
. . . . . . . 8
   SCon
SCon               
               ![[,] [,]](_icc.gif)       
           |
38 | | isphtpc 22037 |
. . . . . . . 8
    
           ![[,] [,]](_icc.gif)     
             
           ![[,] [,]](_icc.gif)       
             
               ![[,] [,]](_icc.gif)                     |
39 | 37, 38 | sylib 200 |
. . . . . . 7
   SCon
SCon               
  
           ![[,] [,]](_icc.gif)       
             
               ![[,] [,]](_icc.gif)                     |
40 | 39 | simp3d 1023 |
. . . . . 6
   SCon
SCon               
  
               ![[,] [,]](_icc.gif)                    |
41 | | n0 3743 |
. . . . . 6
     
             ![[,] [,]](_icc.gif)     
           
     
             ![[,] [,]](_icc.gif)     
              |
42 | 40, 41 | sylib 200 |
. . . . 5
   SCon
SCon               
     
             ![[,] [,]](_icc.gif)     
              |
43 | | simplr 763 |
. . . . . . . . 9
   SCon
SCon               
SCon |
44 | | tx2cn 20637 |
. . . . . . . . . . 11
  TopOn   TopOn   
            |
45 | 11, 16, 44 | syl2anc 667 |
. . . . . . . . . 10
   SCon
SCon               
            |
46 | | cnco 20294 |
. . . . . . . . . 10
      
                      |
47 | 6, 45, 46 | syl2anc 667 |
. . . . . . . . 9
   SCon
SCon               
            |
48 | 21 | fveq2d 5874 |
. . . . . . . . . 10
   SCon
SCon               
                 
            |
49 | | fvco3 5947 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       
                       |
50 | 28, 29, 49 | sylancl 669 |
. . . . . . . . . 10
   SCon
SCon               
  
            
            |
51 | | fvco3 5947 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       
                       |
52 | 28, 32, 51 | sylancl 669 |
. . . . . . . . . 10
   SCon
SCon               
  
            
            |
53 | 48, 50, 52 | 3eqtr4d 2497 |
. . . . . . . . 9
   SCon
SCon               
  
                       |
54 | | sconpht 29964 |
. . . . . . . . 9
  SCon  
            
         
                         ![[,] [,]](_icc.gif)       
           |
55 | 43, 47, 53, 54 | syl3anc 1269 |
. . . . . . . 8
   SCon
SCon               
               ![[,] [,]](_icc.gif)       
           |
56 | | isphtpc 22037 |
. . . . . . . 8
    
           ![[,] [,]](_icc.gif)     
             
           ![[,] [,]](_icc.gif)       
             
               ![[,] [,]](_icc.gif)                     |
57 | 55, 56 | sylib 200 |
. . . . . . 7
   SCon
SCon               
  
           ![[,] [,]](_icc.gif)       
             
               ![[,] [,]](_icc.gif)                     |
58 | 57 | simp3d 1023 |
. . . . . 6
   SCon
SCon               
  
               ![[,] [,]](_icc.gif)                    |
59 | | n0 3743 |
. . . . . 6
     
             ![[,] [,]](_icc.gif)     
           

  
               ![[,] [,]](_icc.gif)                    |
60 | 58, 59 | sylib 200 |
. . . . 5
   SCon
SCon               

  
               ![[,] [,]](_icc.gif)                    |
61 | | eeanv 2080 |
. . . . . 6
          
             ![[,] [,]](_icc.gif)     
                              ![[,] [,]](_icc.gif)       
               
               ![[,] [,]](_icc.gif)                     
               ![[,] [,]](_icc.gif)                     |
62 | 8 | adantr 467 |
. . . . . . . . 9
    SCon
SCon                     
             ![[,] [,]](_icc.gif)     
                              ![[,] [,]](_icc.gif)       
           
  |
63 | 13 | adantr 467 |
. . . . . . . . 9
    SCon
SCon                     
             ![[,] [,]](_icc.gif)     
                              ![[,] [,]](_icc.gif)       
           
  |
64 | 6 | adantr 467 |
. . . . . . . . 9
    SCon
SCon                     
             ![[,] [,]](_icc.gif)     
                              ![[,] [,]](_icc.gif)       
           

     |
65 | | eqid 2453 |
. . . . . . . . 9
 
               |
66 | | eqid 2453 |
. . . . . . . . 9
 
               |
67 | | simprl 765 |
. . . . . . . . 9
    SCon
SCon                     
             ![[,] [,]](_icc.gif)     
                              ![[,] [,]](_icc.gif)       
           
                  ![[,] [,]](_icc.gif)       
            |
68 | | simprr 767 |
. . . . . . . . 9
    SCon
SCon                     
             ![[,] [,]](_icc.gif)     
                              ![[,] [,]](_icc.gif)       
           
                  ![[,] [,]](_icc.gif)       
            |
69 | 62, 63, 64, 65, 66, 67, 68 | txsconlem 29975 |
. . . . . . . 8
    SCon
SCon                     
             ![[,] [,]](_icc.gif)     
                              ![[,] [,]](_icc.gif)       
           
         ![[,] [,]](_icc.gif)           |
70 | 69 | ex 436 |
. . . . . . 7
   SCon
SCon               
      
             ![[,] [,]](_icc.gif)     
                              ![[,] [,]](_icc.gif)       
                    ![[,] [,]](_icc.gif)            |
71 | 70 | exlimdvv 1782 |
. . . . . 6
   SCon
SCon               
        
               ![[,] [,]](_icc.gif)                      
             ![[,] [,]](_icc.gif)     
                      ![[,] [,]](_icc.gif)            |
72 | 61, 71 | syl5bir 222 |
. . . . 5
   SCon
SCon               
  
                  ![[,] [,]](_icc.gif)       
               
             ![[,] [,]](_icc.gif)     
                      ![[,] [,]](_icc.gif)            |
73 | 42, 60, 72 | mp2and 686 |
. . . 4
   SCon
SCon               
         ![[,] [,]](_icc.gif)           |
74 | 73 | expr 620 |
. . 3
   SCon
SCon     
                  ![[,] [,]](_icc.gif)            |
75 | 74 | ralrimiva 2804 |
. 2
  SCon SCon
                        ![[,] [,]](_icc.gif)            |
76 | | isscon 29961 |
. 2
   SCon    PCon                         ![[,] [,]](_icc.gif)             |
77 | 4, 75, 76 | sylanbrc 671 |
1
  SCon SCon
  SCon |