Step | Hyp | Ref
| Expression |
1 | | wal 134 |
. . . . . . 7
       |
2 | | wex 139 |
. . . . . . . . 9
       |
3 | | wal 134 |
. . . . . . . . . . 11
       |
4 | | wim 137 |
. . . . . . . . . . . . 13
  
   |
5 | | axrep.1 |
. . . . . . . . . . . . . . 15
   |
6 | 5 | wl 66 |
. . . . . . . . . . . . . 14
        |
7 | 3, 6 | wc 50 |
. . . . . . . . . . . . 13
         |
8 | | wv 64 |
. . . . . . . . . . . . . 14
     |
9 | | wv 64 |
. . . . . . . . . . . . . 14
     |
10 | 8, 9 | weqi 76 |
. . . . . . . . . . . . 13
      ![]](rbrack.gif)   |
11 | 4, 7, 10 | wov 72 |
. . . . . . . . . . . 12
             ![]](rbrack.gif) ![]](rbrack.gif)   |
12 | 11 | wl 66 |
. . . . . . . . . . 11
                ![]](rbrack.gif) ![]](rbrack.gif)     |
13 | 3, 12 | wc 50 |
. . . . . . . . . 10
                  ![]](rbrack.gif) ![]](rbrack.gif)    |
14 | 13 | wl 66 |
. . . . . . . . 9
                     ![]](rbrack.gif) ![]](rbrack.gif)      |
15 | 2, 14 | wc 50 |
. . . . . . . 8
                       ![]](rbrack.gif) ![]](rbrack.gif)     |
16 | 15 | wl 66 |
. . . . . . 7
                          ![]](rbrack.gif) ![]](rbrack.gif)       |
17 | 1, 16 | wc 50 |
. . . . . 6
                            ![]](rbrack.gif) ![]](rbrack.gif)      |
18 | | wtru 43 |
. . . . . . . 8
   |
19 | | wex 139 |
. . . . . . . . 9
       |
20 | | wan 136 |
. . . . . . . . . . 11
  
   |
21 | | axrep.2 |
. . . . . . . . . . . 12
     |
22 | | wv 64 |
. . . . . . . . . . . 12
     |
23 | 21, 22 | wc 50 |
. . . . . . . . . . 11
        |
24 | 20, 23, 7 | wov 72 |
. . . . . . . . . 10
     
       ![]](rbrack.gif)   |
25 | 24 | wl 66 |
. . . . . . . . 9
        
       ![]](rbrack.gif)     |
26 | 19, 25 | wc 50 |
. . . . . . . 8
                  ![]](rbrack.gif)    |
27 | 18, 26 | eqid 83 |
. . . . . . 7
                   ![]](rbrack.gif)                   ![]](rbrack.gif)  ![]](rbrack.gif) |
28 | 27 | alrimiv 151 |
. . . . . 6
                
       ![]](rbrack.gif)                   ![]](rbrack.gif)  ![]](rbrack.gif)  |
29 | 17, 28 | a1i 28 |
. . . . 5
                            ![]](rbrack.gif) ![]](rbrack.gif)                   
       ![]](rbrack.gif)                   ![]](rbrack.gif)  ![]](rbrack.gif)  |
30 | 29 | ax-cb1 29 |
. . . . . 6
                            ![]](rbrack.gif) ![]](rbrack.gif)      |
31 | | wv 64 |
. . . . . . . . . . 11
         |
32 | 31, 8 | wc 50 |
. . . . . . . . . 10
            |
33 | 32, 26 | weqi 76 |
. . . . . . . . 9
                    
       ![]](rbrack.gif)  ![]](rbrack.gif)   |
34 | 33 | wl 66 |
. . . . . . . 8
                       
       ![]](rbrack.gif)  ![]](rbrack.gif)     |
35 | 3, 34 | wc 50 |
. . . . . . 7
                                 ![]](rbrack.gif)  ![]](rbrack.gif)    |
36 | 26 | wl 66 |
. . . . . . 7
                     ![]](rbrack.gif)      |
37 | | weq 41 |
. . . . . . . . . 10
  
   |
38 | 31, 36 | weqi 76 |
. . . . . . . . . . . . 13
                          ![]](rbrack.gif)  ![]](rbrack.gif)   |
39 | 38 | id 25 |
. . . . . . . . . . . 12
                          ![]](rbrack.gif)                            ![]](rbrack.gif)  ![]](rbrack.gif) |
40 | 31, 8, 39 | ceq1 89 |
. . . . . . . . . . 11
                          ![]](rbrack.gif)                                  ![]](rbrack.gif)      ![]](rbrack.gif) |
41 | 26 | beta 92 |
. . . . . . . . . . . 12
                       ![]](rbrack.gif)                       ![]](rbrack.gif)  ![]](rbrack.gif) |
42 | 38, 41 | a1i 28 |
. . . . . . . . . . 11
                          ![]](rbrack.gif)                         ![]](rbrack.gif)                       ![]](rbrack.gif)  ![]](rbrack.gif) |
43 | 32, 40, 42 | eqtri 95 |
. . . . . . . . . 10
                          ![]](rbrack.gif)                              ![]](rbrack.gif)  ![]](rbrack.gif) |
44 | 37, 32, 26, 43 | oveq1 99 |
. . . . . . . . 9
                          ![]](rbrack.gif)                               ![]](rbrack.gif)                     ![]](rbrack.gif)                   ![]](rbrack.gif)  ![]](rbrack.gif) ![]](rbrack.gif) |
45 | | weq 41 |
. . . . . . . . . 10
          |
46 | | wv 64 |
. . . . . . . . . 10
     |
47 | 37, 46 | ax-17 105 |
. . . . . . . . . 10
        ![]](rbrack.gif) |
48 | 31, 46 | ax-17 105 |
. . . . . . . . . 10
                  ![]](rbrack.gif) |
49 | 26, 46 | ax-hbl1 103 |
. . . . . . . . . 10
                          ![]](rbrack.gif)                          ![]](rbrack.gif)  ![]](rbrack.gif) |
50 | 45, 31, 46, 36, 47, 48, 49 | hbov 111 |
. . . . . . . . 9
                               ![]](rbrack.gif)  ![]](rbrack.gif)                              ![]](rbrack.gif)  ![]](rbrack.gif) ![]](rbrack.gif) |
51 | 33, 44, 50 | leqf 181 |
. . . . . . . 8
                          ![]](rbrack.gif)                                  ![]](rbrack.gif)                        ![]](rbrack.gif)                   ![]](rbrack.gif)  ![]](rbrack.gif) ![]](rbrack.gif) |
52 | 3, 34, 51 | ceq2 90 |
. . . . . . 7
                          ![]](rbrack.gif)                                    ![]](rbrack.gif)  ![]](rbrack.gif)                         ![]](rbrack.gif)                   ![]](rbrack.gif)  ![]](rbrack.gif)  ![]](rbrack.gif) |
53 | 26, 26 | weqi 76 |
. . . . . . . . 9
                   ![]](rbrack.gif)                   ![]](rbrack.gif)  ![]](rbrack.gif)   |
54 | 53 | wl 66 |
. . . . . . . 8
                      ![]](rbrack.gif)                   ![]](rbrack.gif)  ![]](rbrack.gif)     |
55 | | wv 64 |
. . . . . . . 8
         |
56 | 3, 55 | ax-17 105 |
. . . . . . . 8
              ![]](rbrack.gif) |
57 | | weq 41 |
. . . . . . . . . . 11
  
   |
58 | 57, 55 | ax-17 105 |
. . . . . . . . . 10
            ![]](rbrack.gif) |
59 | 2, 55 | ax-17 105 |
. . . . . . . . . . 11
              ![]](rbrack.gif) |
60 | 20, 55 | ax-17 105 |
. . . . . . . . . . . . 13
            ![]](rbrack.gif) |
61 | 23, 55 | ax-17 105 |
. . . . . . . . . . . . 13
                        ![]](rbrack.gif) |
62 | 5, 55, 18 | hbl1 104 |
. . . . . . . . . . . . . 14
                    ![]](rbrack.gif) |
63 | 3, 6, 55, 56, 62 | hbc 110 |
. . . . . . . . . . . . 13
                          ![]](rbrack.gif) |
64 | 20, 23, 55, 7, 60, 61, 63 | hbov 111 |
. . . . . . . . . . . 12
                    ![]](rbrack.gif)           
       ![]](rbrack.gif) ![]](rbrack.gif) |
65 | 24, 55, 64 | hbl 112 |
. . . . . . . . . . 11
                       ![]](rbrack.gif)              
       ![]](rbrack.gif) ![]](rbrack.gif) |
66 | 19, 25, 55, 59, 65 | hbc 110 |
. . . . . . . . . 10
                         ![]](rbrack.gif)                         ![]](rbrack.gif)  ![]](rbrack.gif) |
67 | 37, 26, 55, 26, 58, 66, 66 | hbov 111 |
. . . . . . . . 9
                          ![]](rbrack.gif)                   ![]](rbrack.gif)  ![]](rbrack.gif)                 
       ![]](rbrack.gif)                   ![]](rbrack.gif)  ![]](rbrack.gif) ![]](rbrack.gif) |
68 | 53, 55, 67 | hbl 112 |
. . . . . . . 8
                             ![]](rbrack.gif)                   ![]](rbrack.gif)  ![]](rbrack.gif)                    
       ![]](rbrack.gif)                   ![]](rbrack.gif)  ![]](rbrack.gif) ![]](rbrack.gif) |
69 | 3, 54, 55, 56, 68 | hbc 110 |
. . . . . . 7
                       
       ![]](rbrack.gif)                   ![]](rbrack.gif)  ![]](rbrack.gif)                               ![]](rbrack.gif)                   ![]](rbrack.gif)  ![]](rbrack.gif)  ![]](rbrack.gif) |
70 | 26, 55, 66 | hbl 112 |
. . . . . . 7
                            ![]](rbrack.gif)                            ![]](rbrack.gif)  ![]](rbrack.gif) |
71 | 35, 36, 52, 69, 70 | clf 115 |
. . . . . 6
                                        ![]](rbrack.gif)  ![]](rbrack.gif)                       ![]](rbrack.gif)                          ![]](rbrack.gif)                   ![]](rbrack.gif)  ![]](rbrack.gif)  ![]](rbrack.gif) |
72 | 30, 71 | a1i 28 |
. . . . 5
                            ![]](rbrack.gif) ![]](rbrack.gif)                                           ![]](rbrack.gif)  ![]](rbrack.gif)                       ![]](rbrack.gif)                          ![]](rbrack.gif)                   ![]](rbrack.gif)  ![]](rbrack.gif)  ![]](rbrack.gif) |
73 | 29, 72 | mpbir 87 |
. . . 4
                            ![]](rbrack.gif) ![]](rbrack.gif)                                          ![]](rbrack.gif)  ![]](rbrack.gif)                       ![]](rbrack.gif)   |
74 | 35 | wl 66 |
. . . . 5
                                      ![]](rbrack.gif)  ![]](rbrack.gif)     
  |
75 | 74, 36 | ax4e 168 |
. . . 4
                                       ![]](rbrack.gif)  ![]](rbrack.gif)                       ![]](rbrack.gif)                                          ![]](rbrack.gif)  ![]](rbrack.gif)   |
76 | 73, 75 | syl 16 |
. . 3
                            ![]](rbrack.gif) ![]](rbrack.gif)                                           ![]](rbrack.gif)  ![]](rbrack.gif)   |
77 | 76, 18 | adantl 56 |
. 2
 
                            ![]](rbrack.gif) ![]](rbrack.gif)                                            ![]](rbrack.gif)  ![]](rbrack.gif)   |
78 | 77 | ex 158 |
1
                             ![]](rbrack.gif) ![]](rbrack.gif)                                           ![]](rbrack.gif)  ![]](rbrack.gif)   ![]](rbrack.gif) |