Step | Hyp | Ref
| Expression |
1 | | wat 193 |
. . 3
       |
2 | | wor 140 |
. . . . 5
  
   |
3 | | wv 64 |
. . . . 5
     |
4 | | exmid.1 |
. . . . 5
   |
5 | 2, 3, 4 | wov 72 |
. . . 4
    ![]](rbrack.gif)   |
6 | 5 | wl 66 |
. . 3
       ![]](rbrack.gif)     |
7 | 1, 6 | wc 50 |
. 2
         ![]](rbrack.gif)    |
8 | | wnot 138 |
. . . 4
    |
9 | 8, 4 | wc 50 |
. . 3
     |
10 | 2, 4, 9 | wov 72 |
. 2
    ![]](rbrack.gif)   |
11 | | wtru 43 |
. . . . . 6
   |
12 | 11, 4 | orc 165 |
. . . . 5
  ![]](rbrack.gif) |
13 | 3, 11 | weqi 76 |
. . . . . . . 8
    ![]](rbrack.gif)   |
14 | 13 | id 25 |
. . . . . . 7
        ![]](rbrack.gif) |
15 | 2, 3, 4, 14 | oveq1 99 |
. . . . . 6
        

 ![]](rbrack.gif) ![]](rbrack.gif) |
16 | 5, 11, 15 | cl 116 |
. . . . 5
         ![]](rbrack.gif)    ![]](rbrack.gif) ![]](rbrack.gif) |
17 | 12, 16 | mpbir 87 |
. . . 4
        ![]](rbrack.gif)   |
18 | 6, 11 | ac 197 |
. . . 4
        ![]](rbrack.gif)          ![]](rbrack.gif)          ![]](rbrack.gif)   |
19 | 17, 18 | syl 16 |
. . 3
        ![]](rbrack.gif)          ![]](rbrack.gif)   |
20 | 3, 7 | weqi 76 |
. . . . . 6
            ![]](rbrack.gif)  ![]](rbrack.gif)   |
21 | 20 | id 25 |
. . . . 5
            ![]](rbrack.gif)              ![]](rbrack.gif)  ![]](rbrack.gif) |
22 | 2, 3, 4, 21 | oveq1 99 |
. . . 4
            ![]](rbrack.gif)                 ![]](rbrack.gif)  ![]](rbrack.gif) ![]](rbrack.gif) |
23 | | wv 64 |
. . . . 5
     |
24 | 2, 23 | ax-17 105 |
. . . . 5
        ![]](rbrack.gif) |
25 | 1, 23 | ax-17 105 |
. . . . . 6
          ![]](rbrack.gif) |
26 | 5, 23 | ax-hbl1 103 |
. . . . . 6
            ![]](rbrack.gif)           ![]](rbrack.gif) ![]](rbrack.gif) |
27 | 1, 6, 23, 25, 26 | hbc 110 |
. . . . 5
              ![]](rbrack.gif)              ![]](rbrack.gif)  ![]](rbrack.gif) |
28 | 4, 23 | ax-17 105 |
. . . . 5
          ![]](rbrack.gif) |
29 | 2, 7, 23, 4, 24, 27, 28 | hbov 111 |
. . . 4
               ![]](rbrack.gif)  ![]](rbrack.gif)              ![]](rbrack.gif)  ![]](rbrack.gif) ![]](rbrack.gif) |
30 | 5, 7, 22, 29, 27 | clf 115 |
. . 3
         ![]](rbrack.gif)          ![]](rbrack.gif)            ![]](rbrack.gif)  ![]](rbrack.gif) ![]](rbrack.gif) |
31 | 19, 30 | mpbi 82 |
. 2
          ![]](rbrack.gif)  ![]](rbrack.gif) |
32 | 8, 3 | wc 50 |
. . . . . . . 8
       |
33 | 2, 32, 4 | wov 72 |
. . . . . . 7
    
 ![]](rbrack.gif)   |
34 | 33 | wl 66 |
. . . . . 6
       
 ![]](rbrack.gif)     |
35 | 1, 34 | wc 50 |
. . . . 5
           ![]](rbrack.gif)    |
36 | 8, 35 | wc 50 |
. . . 4
            ![]](rbrack.gif)     |
37 | | wfal 135 |
. . . . . . . . 9
   |
38 | 3, 37 | weqi 76 |
. . . . . . . . . . . . 13
    ![]](rbrack.gif)   |
39 | 38 | id 25 |
. . . . . . . . . . . 12
        ![]](rbrack.gif) |
40 | 8, 3, 39 | ceq2 90 |
. . . . . . . . . . 11
            ![]](rbrack.gif) |
41 | 11, 37 | simpr 23 |
. . . . . . . . . . . . . . . 16
 
  |
42 | 41 | ex 158 |
. . . . . . . . . . . . . . 15
  ![]](rbrack.gif) |
43 | 37 | notval 145 |
. . . . . . . . . . . . . . 15
     ![]](rbrack.gif) ![]](rbrack.gif) |
44 | 42, 43 | mpbir 87 |
. . . . . . . . . . . . . 14
   |
45 | 44 | eqtru 86 |
. . . . . . . . . . . . 13
    ![]](rbrack.gif) |
46 | 11, 45 | eqcomi 79 |
. . . . . . . . . . . 12
    ![]](rbrack.gif) |
47 | 38, 46 | a1i 28 |
. . . . . . . . . . 11
        ![]](rbrack.gif) |
48 | 32, 40, 47 | eqtri 95 |
. . . . . . . . . 10
          ![]](rbrack.gif) |
49 | 2, 32, 4, 48 | oveq1 99 |
. . . . . . . . 9
             ![]](rbrack.gif) ![]](rbrack.gif) |
50 | 33, 37, 49 | cl 116 |
. . . . . . . 8
         
 ![]](rbrack.gif)  
 ![]](rbrack.gif) ![]](rbrack.gif) |
51 | 12, 50 | mpbir 87 |
. . . . . . 7
        
 ![]](rbrack.gif)   |
52 | 34, 37 | ac 197 |
. . . . . . 7
          ![]](rbrack.gif)          
 ![]](rbrack.gif)          
 ![]](rbrack.gif)   |
53 | 51, 52 | syl 16 |
. . . . . 6
        
 ![]](rbrack.gif)          
 ![]](rbrack.gif)   |
54 | 3, 35 | weqi 76 |
. . . . . . . . . 10
              ![]](rbrack.gif)  ![]](rbrack.gif)   |
55 | 54 | id 25 |
. . . . . . . . 9
              ![]](rbrack.gif)                ![]](rbrack.gif)  ![]](rbrack.gif) |
56 | 8, 3, 55 | ceq2 90 |
. . . . . . . 8
              ![]](rbrack.gif)                   ![]](rbrack.gif)   ![]](rbrack.gif) |
57 | 2, 32, 4, 56 | oveq1 99 |
. . . . . . 7
              ![]](rbrack.gif)       
              ![]](rbrack.gif)   ![]](rbrack.gif) ![]](rbrack.gif) |
58 | 8, 23 | ax-17 105 |
. . . . . . . . 9
        ![]](rbrack.gif) |
59 | 33, 23 | ax-hbl1 103 |
. . . . . . . . . 10
            
 ![]](rbrack.gif)             ![]](rbrack.gif) ![]](rbrack.gif) |
60 | 1, 34, 23, 25, 59 | hbc 110 |
. . . . . . . . 9
                ![]](rbrack.gif)              
 ![]](rbrack.gif)  ![]](rbrack.gif) |
61 | 8, 35, 23, 58, 60 | hbc 110 |
. . . . . . . 8
               
 ![]](rbrack.gif)                  ![]](rbrack.gif)   ![]](rbrack.gif) |
62 | 2, 36, 23, 4, 24, 61, 28 | hbov 111 |
. . . . . . 7
                  ![]](rbrack.gif)   ![]](rbrack.gif)                 ![]](rbrack.gif)   ![]](rbrack.gif) ![]](rbrack.gif) |
63 | 33, 35, 57, 62, 60 | clf 115 |
. . . . . 6
         
 ![]](rbrack.gif)          
 ![]](rbrack.gif)               ![]](rbrack.gif)   ![]](rbrack.gif) ![]](rbrack.gif) |
64 | 53, 63 | mpbi 82 |
. . . . 5
             ![]](rbrack.gif)   ![]](rbrack.gif) |
65 | 7, 64 | a1i 28 |
. . . 4
         ![]](rbrack.gif)              ![]](rbrack.gif)   ![]](rbrack.gif) |
66 | 7, 36 | wct 48 |
. . . . . . . . . . 11
          ![]](rbrack.gif)              ![]](rbrack.gif)      |
67 | 66, 4 | simpl 22 |
. . . . . . . . . 10
           ![]](rbrack.gif)              ![]](rbrack.gif)               ![]](rbrack.gif)              ![]](rbrack.gif)    |
68 | 67 | simpld 37 |
. . . . . . . . 9
           ![]](rbrack.gif)              ![]](rbrack.gif)              ![]](rbrack.gif)  |
69 | 3, 4 | olc 164 |
. . . . . . . . . . . . . . 15
    ![]](rbrack.gif) |
70 | 69 | eqtru 86 |
. . . . . . . . . . . . . 14
     ![]](rbrack.gif) ![]](rbrack.gif) |
71 | 11, 70 | eqcomi 79 |
. . . . . . . . . . . . 13
      ![]](rbrack.gif) |
72 | 32, 4 | olc 164 |
. . . . . . . . . . . . . 14
      ![]](rbrack.gif) |
73 | 72 | eqtru 86 |
. . . . . . . . . . . . 13
       ![]](rbrack.gif) ![]](rbrack.gif) |
74 | 5, 71, 73 | eqtri 95 |
. . . . . . . . . . . 12
           ![]](rbrack.gif) ![]](rbrack.gif) |
75 | 5, 74 | leq 91 |
. . . . . . . . . . 11
                 ![]](rbrack.gif) ![]](rbrack.gif) |
76 | 1, 6, 75 | ceq2 90 |
. . . . . . . . . 10
          ![]](rbrack.gif)            ![]](rbrack.gif)  ![]](rbrack.gif) |
77 | 76, 66 | adantl 56 |
. . . . . . . . 9
           ![]](rbrack.gif)              ![]](rbrack.gif)               ![]](rbrack.gif)            ![]](rbrack.gif)  ![]](rbrack.gif) |
78 | 68, 77 | mpbi 82 |
. . . . . . . 8
           ![]](rbrack.gif)              ![]](rbrack.gif)                ![]](rbrack.gif)  |
79 | 67 | simprd 38 |
. . . . . . . . 9
           ![]](rbrack.gif)              ![]](rbrack.gif)     
           ![]](rbrack.gif)   |
80 | 67 | ax-cb1 29 |
. . . . . . . . . 10
           ![]](rbrack.gif)              ![]](rbrack.gif)        |
81 | 35 | notval 145 |
. . . . . . . . . 10
             ![]](rbrack.gif)              ![]](rbrack.gif)  ![]](rbrack.gif) ![]](rbrack.gif) |
82 | 80, 81 | a1i 28 |
. . . . . . . . 9
           ![]](rbrack.gif)              ![]](rbrack.gif)                  ![]](rbrack.gif)              ![]](rbrack.gif)  ![]](rbrack.gif) ![]](rbrack.gif) |
83 | 79, 82 | mpbi 82 |
. . . . . . . 8
           ![]](rbrack.gif)              ![]](rbrack.gif)                 ![]](rbrack.gif)  ![]](rbrack.gif) |
84 | 37, 78, 83 | mpd 156 |
. . . . . . 7
           ![]](rbrack.gif)              ![]](rbrack.gif)      |
85 | 84 | ex 158 |
. . . . . 6
          ![]](rbrack.gif)              ![]](rbrack.gif)     ![]](rbrack.gif) |
86 | 4 | notval 145 |
. . . . . . 7
     ![]](rbrack.gif) ![]](rbrack.gif) |
87 | 66, 86 | a1i 28 |
. . . . . 6
          ![]](rbrack.gif)              ![]](rbrack.gif)        ![]](rbrack.gif) ![]](rbrack.gif) |
88 | 85, 87 | mpbir 87 |
. . . . 5
          ![]](rbrack.gif)              ![]](rbrack.gif)      |
89 | 4, 9 | olc 164 |
. . . . 5
      ![]](rbrack.gif) |
90 | 88, 89 | syl 16 |
. . . 4
          ![]](rbrack.gif)              ![]](rbrack.gif)       ![]](rbrack.gif) |
91 | 4, 9 | orc 165 |
. . . . 5
    ![]](rbrack.gif) |
92 | 91, 7 | adantl 56 |
. . . 4
          ![]](rbrack.gif)  
    ![]](rbrack.gif) |
93 | 36, 4, 10, 65, 90, 92 | ecase 163 |
. . 3
         ![]](rbrack.gif)     ![]](rbrack.gif) |
94 | 93, 11 | adantl 56 |
. 2
 
         ![]](rbrack.gif)      ![]](rbrack.gif) |
95 | 91, 11 | adantl 56 |
. 2
 
     ![]](rbrack.gif) |
96 | 7, 4, 10, 31, 94, 95 | ecase 163 |
1
    ![]](rbrack.gif) |