Step | Hyp | Ref
| Expression |
1 | | wal 134 |
. . . . . . . 8
       |
2 | | ax11.1 |
. . . . . . . . 9
   |
3 | 2 | wl 66 |
. . . . . . . 8
        |
4 | 1, 3 | wc 50 |
. . . . . . 7
         |
5 | 4 | id 25 |
. . . . . 6
             |
6 | | wv 64 |
. . . . . . . . . 10
     |
7 | 3, 6 | wc 50 |
. . . . . . . . 9
           |
8 | 7 | wl 66 |
. . . . . . . 8
                |
9 | 3 | eta 178 |
. . . . . . . 8
                ![]](rbrack.gif) |
10 | 1, 8, 9 | ceq2 90 |
. . . . . . 7
                      ![]](rbrack.gif) |
11 | 4, 10 | a1i 28 |
. . . . . 6
                            ![]](rbrack.gif) |
12 | 5, 11 | mpbir 87 |
. . . . 5
                     |
13 | | wim 137 |
. . . . . . . . 9
  
   |
14 | | wv 64 |
. . . . . . . . . 10
     |
15 | 6, 14 | weqi 76 |
. . . . . . . . 9
      ![]](rbrack.gif)   |
16 | 13, 15, 2 | wov 72 |
. . . . . . . 8
        ![]](rbrack.gif)   |
17 | 16 | wl 66 |
. . . . . . 7
           ![]](rbrack.gif)     |
18 | 1, 17 | wc 50 |
. . . . . 6
             ![]](rbrack.gif)    |
19 | 1, 8 | wc 50 |
. . . . . . 7
                 |
20 | 19 | id 25 |
. . . . . 6
                             |
21 | 15, 4 | simpr 23 |
. . . . . . . . . . 11
       ![]](rbrack.gif)
              |
22 | 21 | ax-cb1 29 |
. . . . . . . . . . . 12
       ![]](rbrack.gif)
          |
23 | 22, 10 | a1i 28 |
. . . . . . . . . . 11
       ![]](rbrack.gif)
                             ![]](rbrack.gif) |
24 | 21, 23 | mpbir 87 |
. . . . . . . . . 10
       ![]](rbrack.gif)
                      |
25 | 24 | ax-cb2 30 |
. . . . . . . . 9
                 |
26 | 13, 25, 18 | wov 72 |
. . . . . . . 8
                            ![]](rbrack.gif)  ![]](rbrack.gif)   |
27 | 7, 15 | simpl 22 |
. . . . . . . . . . . . 13
                ![]](rbrack.gif)          |
28 | 7, 15 | simpr 23 |
. . . . . . . . . . . . . . 15
                ![]](rbrack.gif)       ![]](rbrack.gif) |
29 | 3, 6, 28 | ceq2 90 |
. . . . . . . . . . . . . 14
                ![]](rbrack.gif)                   ![]](rbrack.gif) |
30 | 7, 15 | wct 48 |
. . . . . . . . . . . . . . 15
                ![]](rbrack.gif)    |
31 | 2 | beta 92 |
. . . . . . . . . . . . . . 15
          ![]](rbrack.gif) |
32 | 30, 31 | a1i 28 |
. . . . . . . . . . . . . 14
                ![]](rbrack.gif)           ![]](rbrack.gif) |
33 | 7, 29, 32 | eqtri 95 |
. . . . . . . . . . . . 13
                ![]](rbrack.gif)           ![]](rbrack.gif) |
34 | 27, 33 | mpbi 82 |
. . . . . . . . . . . 12
                ![]](rbrack.gif)  |
35 | 34 | ex 158 |
. . . . . . . . . . 11
       
        ![]](rbrack.gif) |
36 | | wtru 43 |
. . . . . . . . . . 11
   |
37 | 35, 36 | adantl 56 |
. . . . . . . . . 10
 
                 ![]](rbrack.gif) |
38 | 37 | ex 158 |
. . . . . . . . 9
                 ![]](rbrack.gif) ![]](rbrack.gif) |
39 | 38 | alrimiv 151 |
. . . . . . . 8
                      ![]](rbrack.gif) ![]](rbrack.gif)  |
40 | 7, 16 | ax5 207 |
. . . . . . . 8
                       ![]](rbrack.gif) ![]](rbrack.gif)                             ![]](rbrack.gif)  ![]](rbrack.gif) ![]](rbrack.gif) |
41 | 26, 39, 40 | mpd 156 |
. . . . . . 7
                            ![]](rbrack.gif)  ![]](rbrack.gif) |
42 | 19, 41 | a1i 28 |
. . . . . 6
                                          ![]](rbrack.gif)  ![]](rbrack.gif) |
43 | 18, 20, 42 | mpd 156 |
. . . . 5
                           ![]](rbrack.gif)  |
44 | 12, 43 | syl 16 |
. . . 4
                   ![]](rbrack.gif)  |
45 | 36, 15 | wct 48 |
. . . 4
 
  
   ![]](rbrack.gif)    |
46 | 44, 45 | adantl 56 |
. . 3
         ![]](rbrack.gif)                      ![]](rbrack.gif)  |
47 | 46 | ex 158 |
. 2
 
  
   ![]](rbrack.gif)                     ![]](rbrack.gif)  ![]](rbrack.gif) |
48 | 47 | ex 158 |
1
                           ![]](rbrack.gif)  ![]](rbrack.gif) ![]](rbrack.gif) |