Proof of Theorem sbcomxyyz
Step | Hyp | Ref
| Expression |
1 | | ax-bndl 1396 |
. 2
 
       
    |
2 | | ax-ial 1424 |
. . . . 5
 
  
  |
3 | | drsb1 1677 |
. . . . 5
 
   ![]](rbrack.gif)   ![]](rbrack.gif)    |
4 | 2, 3 | sbbid 1723 |
. . . 4
 
   ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)    |
5 | | drsb1 1677 |
. . . 4
 
   ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)    |
6 | 4, 5 | bitr3d 179 |
. . 3
 
   ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)    |
7 | | sbequ12 1651 |
. . . . . 6
  
 ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)    |
8 | 7 | sps 1427 |
. . . . 5
 
   ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)    |
9 | | hbae 1603 |
. . . . . 6
 
  
  |
10 | | sbequ12 1651 |
. . . . . . 7
    ![]](rbrack.gif)    |
11 | 10 | sps 1427 |
. . . . . 6
 
   ![]](rbrack.gif)    |
12 | 9, 11 | sbbid 1723 |
. . . . 5
 
   ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)    |
13 | 8, 12 | bitr3d 179 |
. . . 4
 
   ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)    |
14 | | df-nf 1347 |
. . . . . 6
     
   |
15 | 14 | albii 1356 |
. . . . 5
             |
16 | | ax-ial 1424 |
. . . . . . 7
           |
17 | | nfs1v 1812 |
. . . . . . . . . 10
  
 ![]](rbrack.gif)  |
18 | 17 | nfsb 1819 |
. . . . . . . . 9
  
 ![]](rbrack.gif)   ![]](rbrack.gif)  |
19 | 18 | a1i 9 |
. . . . . . . 8
      
 ![]](rbrack.gif)   ![]](rbrack.gif)   |
20 | 19 | nfrd 1410 |
. . . . . . 7
       ![]](rbrack.gif)   ![]](rbrack.gif)     ![]](rbrack.gif)   ![]](rbrack.gif)    |
21 | | nfr 1408 |
. . . . . . . . 9
       |
22 | | nfnf1 1433 |
. . . . . . . . . . . . 13
    |
23 | | nfa1 1431 |
. . . . . . . . . . . . 13
  
 |
24 | 22, 23 | nfan 1454 |
. . . . . . . . . . . 12
    
  |
25 | 24 | nfri 1409 |
. . . . . . . . . . 11
   
         |
26 | | nfs1v 1812 |
. . . . . . . . . . . . 13
    ![]](rbrack.gif)   ![]](rbrack.gif)  |
27 | 26 | a1i 9 |
. . . . . . . . . . . 12
   
     ![]](rbrack.gif)   ![]](rbrack.gif)   |
28 | 27 | nfrd 1410 |
. . . . . . . . . . 11
   
    ![]](rbrack.gif)   ![]](rbrack.gif)     ![]](rbrack.gif)   ![]](rbrack.gif)    |
29 | | sbequ12 1651 |
. . . . . . . . . . . . . . 15
    ![]](rbrack.gif)    |
30 | 29, 7 | sylan9bb 435 |
. . . . . . . . . . . . . 14
 
    ![]](rbrack.gif)   ![]](rbrack.gif)    |
31 | 30 | ex 108 |
. . . . . . . . . . . . 13
 
   ![]](rbrack.gif)   ![]](rbrack.gif)     |
32 | 31 | sps 1427 |
. . . . . . . . . . . 12
 
    ![]](rbrack.gif)   ![]](rbrack.gif)     |
33 | 32 | adantl 262 |
. . . . . . . . . . 11
   
     ![]](rbrack.gif)   ![]](rbrack.gif)     |
34 | 25, 28, 33 | sbiedh 1667 |
. . . . . . . . . 10
   
    ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)    |
35 | 34 | ex 108 |
. . . . . . . . 9
     
 ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)     |
36 | 21, 35 | syld 40 |
. . . . . . . 8
      ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)     |
37 | 36 | sps 1427 |
. . . . . . 7
      
 ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)     |
38 | 16, 20, 37 | sbiedh 1667 |
. . . . . 6
       ![]](rbrack.gif)   ![]](rbrack.gif) 
 ![]](rbrack.gif)   ![]](rbrack.gif)    |
39 | 38 | bicomd 129 |
. . . . 5
       ![]](rbrack.gif)   ![]](rbrack.gif) 
 ![]](rbrack.gif)   ![]](rbrack.gif)    |
40 | 15, 39 | sylbir 125 |
. . . 4
      
    ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)    |
41 | 13, 40 | jaoi 635 |
. . 3
  
           ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)    |
42 | 6, 41 | jaoi 635 |
. 2
  
 
     
      ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)   ![]](rbrack.gif)    |
43 | 1, 42 | ax-mp 7 |
1
   ![]](rbrack.gif)   ![]](rbrack.gif) 
 ![]](rbrack.gif)   ![]](rbrack.gif)   |