Step | Hyp | Ref
| Expression |
1 | | itgsubst.x |
. . 3
   |
2 | | itgsubst.y |
. . 3
   |
3 | | itgsubst.le |
. . 3

  |
4 | | ioossre 11693 |
. . . . 5
     |
5 | | ax-resscn 9593 |
. . . . 5
 |
6 | | cncfss 21924 |
. . . . 5
     
    ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)       |
7 | 4, 5, 6 | mp2an 677 |
. . . 4
   ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)      |
8 | | itgsubst.a |
. . . 4
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)           |
9 | 7, 8 | sseldi 3429 |
. . 3
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       |
10 | 1, 2, 3, 9 | evthicc 22403 |
. 2
     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)      
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)         |
11 | | ressxr 9681 |
. . . . . . . 8
 |
12 | 4, 11 | sstri 3440 |
. . . . . . 7
     |
13 | | cncff 21918 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          |
14 | 8, 13 | syl 17 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          |
15 | 14 | adantr 467 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          |
16 | | simprl 763 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)    |
17 | 15, 16 | ffvelrnd 6021 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)            |
18 | 12, 17 | sseldi 3429 |
. . . . . 6
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)        |
19 | | itgsubst.w |
. . . . . . 7
   |
20 | 19 | adantr 467 |
. . . . . 6
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)          |
21 | | eliooord 11691 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)         |
22 | 17, 21 | syl 17 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)     
   |
23 | 22 | simprd 465 |
. . . . . 6
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)        |
24 | | qbtwnxr 11490 |
. . . . . 6
      ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)     
       ![[,] [,]](_icc.gif)     
   |
25 | 18, 20, 23, 24 | syl3anc 1267 |
. . . . 5
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)     
   |
26 | | qre 11266 |
. . . . . . . . . 10
   |
27 | 26 | ad2antrl 733 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)     
  
  |
28 | | itgsubst.z |
. . . . . . . . . . 11
   |
29 | 28 | ad2antrr 731 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)     
  
  |
30 | 18 | adantr 467 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)     
       ![[,] [,]](_icc.gif)        |
31 | 27 | rexrd 9687 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)     
  
  |
32 | 22 | simpld 461 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)        |
33 | 32 | adantr 467 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)     
       ![[,] [,]](_icc.gif)        |
34 | | simprrl 773 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)     
       ![[,] [,]](_icc.gif)        |
35 | 29, 30, 31, 33, 34 | xrlttrd 11453 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)     
     |
36 | | simprrr 774 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)     
     |
37 | 19 | ad2antrr 731 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)     
  
  |
38 | | elioo2 11674 |
. . . . . . . . . 10
       

    |
39 | 29, 37, 38 | syl2anc 666 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)     
             |
40 | 27, 35, 36, 39 | mpbir3and 1190 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)     
  
      |
41 | | anass 654 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       
   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)          |
42 | | simprrl 773 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)     
       ![[,] [,]](_icc.gif)        |
43 | 42 | adantr 467 |
. . . . . . . . . . . . 13
   
  ![[,] [,]](_icc.gif)   
     ![[,] [,]](_icc.gif)     
  
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)        |
44 | 14 | ad2antrr 731 |
. . . . . . . . . . . . . . . 16
     ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)     
      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          |
45 | 44 | ffvelrnda 6020 |
. . . . . . . . . . . . . . 15
   
  ![[,] [,]](_icc.gif)   
     ![[,] [,]](_icc.gif)     
  
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)            |
46 | 12, 45 | sseldi 3429 |
. . . . . . . . . . . . . 14
   
  ![[,] [,]](_icc.gif)   
     ![[,] [,]](_icc.gif)     
  
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)        |
47 | | simplr 761 |
. . . . . . . . . . . . . . . . 17
     ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)     
     ![[,] [,]](_icc.gif)    |
48 | 44, 47 | ffvelrnd 6021 |
. . . . . . . . . . . . . . . 16
     ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)     
       ![[,] [,]](_icc.gif)            |
49 | 12, 48 | sseldi 3429 |
. . . . . . . . . . . . . . 15
     ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)     
       ![[,] [,]](_icc.gif)        |
50 | 49 | adantr 467 |
. . . . . . . . . . . . . 14
   
  ![[,] [,]](_icc.gif)   
     ![[,] [,]](_icc.gif)     
  
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)        |
51 | 26 | ad2antrl 733 |
. . . . . . . . . . . . . . . 16
     ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)     
  
  |
52 | 51 | adantr 467 |
. . . . . . . . . . . . . . 15
   
  ![[,] [,]](_icc.gif)   
     ![[,] [,]](_icc.gif)     
  
  ![[,] [,]](_icc.gif)  
  |
53 | 52 | rexrd 9687 |
. . . . . . . . . . . . . 14
   
  ![[,] [,]](_icc.gif)   
     ![[,] [,]](_icc.gif)     
  
  ![[,] [,]](_icc.gif)  
  |
54 | | xrlelttr 11450 |
. . . . . . . . . . . . . 14
      ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)      
    ![[,] [,]](_icc.gif)         |
55 | 46, 50, 53, 54 | syl3anc 1267 |
. . . . . . . . . . . . 13
   
  ![[,] [,]](_icc.gif)   
     ![[,] [,]](_icc.gif)     
  
  ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)      
    ![[,] [,]](_icc.gif)         |
56 | 43, 55 | mpan2d 679 |
. . . . . . . . . . . 12
   
  ![[,] [,]](_icc.gif)   
     ![[,] [,]](_icc.gif)     
  
  ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)     
   |
57 | 56 | ralimdva 2795 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)     
       ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         |
58 | 57 | imp 431 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)   
     ![[,] [,]](_icc.gif)     
      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)      
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)        |
59 | 58 | an32s 812 |
. . . . . . . . 9
   
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)     
      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)        |
60 | 41, 59 | sylanbr 476 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)     
   
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
  |
61 | 40, 60 | jca 535 |
. . . . . . 7
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)     
           ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         |
62 | 61 | ex 436 |
. . . . . 6
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)     
 
    
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          |
63 | 62 | reximdv2 2857 |
. . . . 5
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         |
64 | 25, 63 | mpd 15 |
. . . 4
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)        |
65 | 64 | rexlimdvaa 2879 |
. . 3
     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         |
66 | 28 | adantr 467 |
. . . . . 6
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)          |
67 | 14 | adantr 467 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          |
68 | | simprl 763 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)    |
69 | 67, 68 | ffvelrnd 6021 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)            |
70 | 12, 69 | sseldi 3429 |
. . . . . 6
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)        |
71 | 69, 21 | syl 17 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)     
   |
72 | 71 | simpld 461 |
. . . . . 6
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)        |
73 | | qbtwnxr 11490 |
. . . . . 6
      ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       

    ![[,] [,]](_icc.gif)         |
74 | 66, 70, 72, 73 | syl3anc 1267 |
. . . . 5
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)         
    ![[,] [,]](_icc.gif)         |
75 | | qre 11266 |
. . . . . . . . . 10
   |
76 | 75 | ad2antrl 733 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)         
    ![[,] [,]](_icc.gif)           |
77 | | simprrl 773 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)         
    ![[,] [,]](_icc.gif)           |
78 | 76 | rexrd 9687 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)         
    ![[,] [,]](_icc.gif)           |
79 | 70 | adantr 467 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)         
    ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)        |
80 | 19 | ad2antrr 731 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)         
    ![[,] [,]](_icc.gif)           |
81 | | simprrr 774 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)         
    ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)        |
82 | 71 | simprd 465 |
. . . . . . . . . . 11
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)        |
83 | 82 | adantr 467 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)         
    ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)     
  |
84 | 78, 79, 80, 81, 83 | xrlttrd 11453 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)         
    ![[,] [,]](_icc.gif)           |
85 | 28 | ad2antrr 731 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)         
    ![[,] [,]](_icc.gif)           |
86 | | elioo2 11674 |
. . . . . . . . . 10
       

    |
87 | 85, 80, 86 | syl2anc 666 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)         
    ![[,] [,]](_icc.gif)             

    |
88 | 76, 77, 84, 87 | mpbir3and 1190 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)         
    ![[,] [,]](_icc.gif)               |
89 | | anass 654 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       
   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)          |
90 | | simprrr 774 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)        |
91 | 90 | adantr 467 |
. . . . . . . . . . . . 13
   
  ![[,] [,]](_icc.gif)   

    ![[,] [,]](_icc.gif)        
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)        |
92 | 75 | ad2antrl 733 |
. . . . . . . . . . . . . . . 16
     ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)           |
93 | 92 | adantr 467 |
. . . . . . . . . . . . . . 15
   
  ![[,] [,]](_icc.gif)   

    ![[,] [,]](_icc.gif)        
  ![[,] [,]](_icc.gif)  
  |
94 | 93 | rexrd 9687 |
. . . . . . . . . . . . . 14
   
  ![[,] [,]](_icc.gif)   

    ![[,] [,]](_icc.gif)        
  ![[,] [,]](_icc.gif)  
  |
95 | 14 | ad2antrr 731 |
. . . . . . . . . . . . . . . . 17
     ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          |
96 | | simplr 761 |
. . . . . . . . . . . . . . . . 17
     ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)    |
97 | 95, 96 | ffvelrnd 6021 |
. . . . . . . . . . . . . . . 16
     ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)            |
98 | 12, 97 | sseldi 3429 |
. . . . . . . . . . . . . . 15
     ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)        |
99 | 98 | adantr 467 |
. . . . . . . . . . . . . 14
   
  ![[,] [,]](_icc.gif)   

    ![[,] [,]](_icc.gif)        
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)        |
100 | 95 | ffvelrnda 6020 |
. . . . . . . . . . . . . . 15
   
  ![[,] [,]](_icc.gif)   

    ![[,] [,]](_icc.gif)        
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)            |
101 | 12, 100 | sseldi 3429 |
. . . . . . . . . . . . . 14
   
  ![[,] [,]](_icc.gif)   

    ![[,] [,]](_icc.gif)        
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)        |
102 | | xrltletr 11451 |
. . . . . . . . . . . . . 14
      ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)      
    ![[,] [,]](_icc.gif)         |
103 | 94, 99, 101, 102 | syl3anc 1267 |
. . . . . . . . . . . . 13
   
  ![[,] [,]](_icc.gif)   

    ![[,] [,]](_icc.gif)        
  ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)      
    ![[,] [,]](_icc.gif)         |
104 | 91, 103 | mpand 680 |
. . . . . . . . . . . 12
   
  ![[,] [,]](_icc.gif)   

    ![[,] [,]](_icc.gif)        
  ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)         |
105 | 104 | ralimdva 2795 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)    
    ![[,] [,]](_icc.gif)          
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         |
106 | 105 | imp 431 |
. . . . . . . . . 10
   
  ![[,] [,]](_icc.gif)   

    ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)      
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)        |
107 | 106 | an32s 812 |
. . . . . . . . 9
   
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)        
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)        |
108 | 89, 107 | sylanbr 476 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)         
    ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)        |
109 | 88, 108 | jca 535 |
. . . . . . 7
      ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
    ![[,] [,]](_icc.gif)         
    ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         |
110 | 109 | ex 436 |
. . . . . 6
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)            
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          |
111 | 110 | reximdv2 2857 |
. . . . 5
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)          
    ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         |
112 | 74, 111 | mpd 15 |
. . . 4
 
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)        |
113 | 112 | rexlimdvaa 2879 |
. . 3
     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         |
114 | | ancom 452 |
. . . . 5
           ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
         ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         |
115 | | reeanv 2957 |
. . . . 5
                 ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)      
 
        ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
         ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         |
116 | 114, 115 | bitr4i 256 |
. . . 4
           ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)                       ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         |
117 | | r19.26 2916 |
. . . . . 6
 
  ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         |
118 | 14 | adantr 467 |
. . . . . . . . . . . 12
 
    
         ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          |
119 | 118 | ffvelrnda 6020 |
. . . . . . . . . . 11
       
        ![[,] [,]](_icc.gif)  
    ![[,] [,]](_icc.gif)            |
120 | 4, 119 | sseldi 3429 |
. . . . . . . . . 10
       
        ![[,] [,]](_icc.gif)  
    ![[,] [,]](_icc.gif)        |
121 | 120 | 3biant1d 1377 |
. . . . . . . . 9
       
        ![[,] [,]](_icc.gif)  
 
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)      
     ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)          |
122 | | simplrl 769 |
. . . . . . . . . . 11
       
        ![[,] [,]](_icc.gif)  
      |
123 | 12, 122 | sseldi 3429 |
. . . . . . . . . 10
       
        ![[,] [,]](_icc.gif)  
  |
124 | | simplrr 770 |
. . . . . . . . . . 11
       
        ![[,] [,]](_icc.gif)  
      |
125 | 12, 124 | sseldi 3429 |
. . . . . . . . . 10
       
        ![[,] [,]](_icc.gif)  
  |
126 | | elioo2 11674 |
. . . . . . . . . 10
        ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)     
    |
127 | 123, 125,
126 | syl2anc 666 |
. . . . . . . . 9
       
        ![[,] [,]](_icc.gif)  
     ![[,] [,]](_icc.gif)         
     ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)          |
128 | 121, 127 | bitr4d 260 |
. . . . . . . 8
       
        ![[,] [,]](_icc.gif)  
 
    ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)      
    ![[,] [,]](_icc.gif)             |
129 | 128 | ralbidva 2823 |
. . . . . . 7
 
    
       
  ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)      
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)             |
130 | | nffvmpt1 5871 |
. . . . . . . . . . . 12
      ![[,] [,]](_icc.gif)       |
131 | 130 | nfel1 2605 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)           |
132 | | nfv 1760 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)           |
133 | | fveq2 5863 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)        |
134 | 133 | eleq1d 2512 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)             |
135 | 131, 132,
134 | cbvral 3014 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)            |
136 | | simpr 463 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)    |
137 | | eqid 2450 |
. . . . . . . . . . . . . . . 16
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
138 | 137 | fmpt 6041 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          |
139 | 14, 138 | sylibr 216 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif)         |
140 | 139 | r19.21bi 2756 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)  
      |
141 | 137 | fvmpt2 5955 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif) 
         ![[,] [,]](_icc.gif)        |
142 | 136, 140,
141 | syl2anc 666 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)  
    ![[,] [,]](_icc.gif)        |
143 | 142 | eleq1d 2512 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)  
     ![[,] [,]](_icc.gif)         
       |
144 | 143 | ralbidva 2823 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          |
145 | 135, 144 | syl5bb 261 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)          |
146 | 145 | adantr 467 |
. . . . . . . 8
 
    
       
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         
   ![[,] [,]](_icc.gif)          |
147 | 1 | adantr 467 |
. . . . . . . . . . 11
 
     
        ![[,] [,]](_icc.gif)           |
148 | 2 | adantr 467 |
. . . . . . . . . . 11
 
     
        ![[,] [,]](_icc.gif)           |
149 | 3 | adantr 467 |
. . . . . . . . . . 11
 
     
        ![[,] [,]](_icc.gif)           |
150 | 28 | adantr 467 |
. . . . . . . . . . 11
 
     
        ![[,] [,]](_icc.gif)           |
151 | 19 | adantr 467 |
. . . . . . . . . . 11
 
     
        ![[,] [,]](_icc.gif)           |
152 | | nfcv 2591 |
. . . . . . . . . . . . . 14
   |
153 | | nfcsb1v 3378 |
. . . . . . . . . . . . . 14
  
 ![]_ ]_](_urbrack.gif)  |
154 | | csbeq1a 3371 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)   |
155 | 152, 153,
154 | cbvmpt 4493 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    ![]_ ]_](_urbrack.gif)   |
156 | 155, 8 | syl5eqelr 2533 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)    ![]_ ]_](_urbrack.gif)     ![[,] [,]](_icc.gif)           |
157 | 156 | adantr 467 |
. . . . . . . . . . 11
 
     
        ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)    ![]_ ]_](_urbrack.gif)     ![[,] [,]](_icc.gif)           |
158 | | nfcv 2591 |
. . . . . . . . . . . . . 14
   |
159 | | nfcsb1v 3378 |
. . . . . . . . . . . . . 14
  
 ![]_ ]_](_urbrack.gif)  |
160 | | csbeq1a 3371 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)   |
161 | 158, 159,
160 | cbvmpt 4493 |
. . . . . . . . . . . . 13
             ![]_ ]_](_urbrack.gif)   |
162 | | itgsubst.b |
. . . . . . . . . . . . 13
                    |
163 | 161, 162 | syl5eqelr 2533 |
. . . . . . . . . . . 12
        ![]_ ]_](_urbrack.gif)               |
164 | 163 | adantr 467 |
. . . . . . . . . . 11
 
     
        ![[,] [,]](_icc.gif)                ![]_ ]_](_urbrack.gif)               |
165 | | nfcv 2591 |
. . . . . . . . . . . . . 14
   |
166 | | nfcsb1v 3378 |
. . . . . . . . . . . . . 14
  
 ![]_ ]_](_urbrack.gif)  |
167 | | csbeq1a 3371 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)   |
168 | 165, 166,
167 | cbvmpt 4493 |
. . . . . . . . . . . . 13
             ![]_ ]_](_urbrack.gif)   |
169 | | itgsubst.c |
. . . . . . . . . . . . 13
                 |
170 | 168, 169 | syl5eqelr 2533 |
. . . . . . . . . . . 12
        ![]_ ]_](_urbrack.gif)            |
171 | 170 | adantr 467 |
. . . . . . . . . . 11
 
     
        ![[,] [,]](_icc.gif)                ![]_ ]_](_urbrack.gif)            |
172 | | itgsubst.da |
. . . . . . . . . . . . 13
     ![[,] [,]](_icc.gif)            |
173 | 155 | oveq2i 6299 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)    ![]_ ]_](_urbrack.gif)    |
174 | 172, 173,
161 | 3eqtr3g 2507 |
. . . . . . . . . . . 12
     ![[,] [,]](_icc.gif)    ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)    |
175 | 174 | adantr 467 |
. . . . . . . . . . 11
 
     
        ![[,] [,]](_icc.gif)             ![[,] [,]](_icc.gif)    ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)    |
176 | | csbeq1 3365 |
. . . . . . . . . . 11
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)
 ![]_ ]_](_urbrack.gif)   |
177 | | csbeq1 3365 |
. . . . . . . . . . 11
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
178 | | csbeq1 3365 |
. . . . . . . . . . 11
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
179 | | simprll 771 |
. . . . . . . . . . 11
 
     
        ![[,] [,]](_icc.gif)               |
180 | | simprlr 772 |
. . . . . . . . . . 11
 
     
        ![[,] [,]](_icc.gif)               |
181 | | simprr 765 |
. . . . . . . . . . . 12
 
     
        ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)         |
182 | 153 | nfel1 2605 |
. . . . . . . . . . . . 13
  
 ![]_ ]_](_urbrack.gif)
     |
183 | 154 | eleq1d 2512 |
. . . . . . . . . . . . 13
 
   
  ![]_ ]_](_urbrack.gif)        |
184 | 182, 183 | rspc 3143 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)         ![]_ ]_](_urbrack.gif)        |
185 | 181, 184 | mpan9 472 |
. . . . . . . . . . 11
                 ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)     ![]_ ]_](_urbrack.gif)       |
186 | 147, 148,
149, 150, 151, 157, 164, 171, 175, 176, 177, 178, 179, 180, 185 | itgsubstlem 22993 |
. . . . . . . . . 10
 
     
        ![[,] [,]](_icc.gif)         _   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  ![] ]](rbrack.gif)   ![]_ ]_](_urbrack.gif)  _  ![] ]](rbrack.gif)     ![]_ ]_](_urbrack.gif)
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
187 | 167, 165,
166 | cbvditg 22802 |
. . . . . . . . . . . 12
_ 
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)  ![] ]](rbrack.gif)  _   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)  ![] ]](rbrack.gif) 
 ![]_ ]_](_urbrack.gif)
  |
188 | | nfcvd 2592 |
. . . . . . . . . . . . . . 15
     |
189 | | itgsubst.k |
. . . . . . . . . . . . . . 15
   |
190 | 188, 189 | csbiegf 3386 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)   |
191 | | ditgeq1 22796 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)
_ 
 ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)  ![] ]](rbrack.gif)  _   ![]_ ]_](_urbrack.gif)  ![] ]](rbrack.gif)    |
192 | 1, 190, 191 | 3syl 18 |
. . . . . . . . . . . . 13
 _   ![]_ ]_](_urbrack.gif) 
 ![]_ ]_](_urbrack.gif)  ![] ]](rbrack.gif)  _   ![]_ ]_](_urbrack.gif)  ![] ]](rbrack.gif)    |
193 | | nfcvd 2592 |
. . . . . . . . . . . . . . 15
     |
194 | | itgsubst.l |
. . . . . . . . . . . . . . 15
   |
195 | 193, 194 | csbiegf 3386 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)   |
196 | | ditgeq2 22797 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)
_   ![]_ ]_](_urbrack.gif)  ![] ]](rbrack.gif)  _  ![] ]](rbrack.gif)    |
197 | 2, 195, 196 | 3syl 18 |
. . . . . . . . . . . . 13
 _ 
 ![]_ ]_](_urbrack.gif)  ![] ]](rbrack.gif)  _  ![] ]](rbrack.gif)    |
198 | 192, 197 | eqtrd 2484 |
. . . . . . . . . . . 12
 _   ![]_ ]_](_urbrack.gif) 
 ![]_ ]_](_urbrack.gif)  ![] ]](rbrack.gif)  _  ![] ]](rbrack.gif)    |
199 | 187, 198 | syl5eqr 2498 |
. . . . . . . . . . 11
 _   ![]_ ]_](_urbrack.gif) 
 ![]_ ]_](_urbrack.gif)  ![] ]](rbrack.gif)   ![]_ ]_](_urbrack.gif)  _  ![] ]](rbrack.gif)    |
200 | 199 | adantr 467 |
. . . . . . . . . 10
 
     
        ![[,] [,]](_icc.gif)         _   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  ![] ]](rbrack.gif)   ![]_ ]_](_urbrack.gif)  _  ![] ]](rbrack.gif)    |
201 | 154 | csbeq1d 3369 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)
 ![]_ ]_](_urbrack.gif)   |
202 | 201, 160 | oveq12d 6306 |
. . . . . . . . . . . . 13
  
 ![]_ ]_](_urbrack.gif)
     ![]_ ]_](_urbrack.gif)  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
203 | | nfcv 2591 |
. . . . . . . . . . . . 13
     ![]_ ]_](_urbrack.gif)
  |
204 | | nfcv 2591 |
. . . . . . . . . . . . . . 15
   |
205 | 153, 204 | nfcsb 3380 |
. . . . . . . . . . . . . 14
     ![]_ ]_](_urbrack.gif)
 ![]_ ]_](_urbrack.gif)  |
206 | | nfcv 2591 |
. . . . . . . . . . . . . 14
  |
207 | 205, 206,
159 | nfov 6314 |
. . . . . . . . . . . . 13
      ![]_ ]_](_urbrack.gif)  ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
208 | 202, 203,
207 | cbvditg 22802 |
. . . . . . . . . . . 12
_  ![] ]](rbrack.gif)    ![]_ ]_](_urbrack.gif)
  _  ![] ]](rbrack.gif)     ![]_ ]_](_urbrack.gif)  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
209 | | ioossicc 11717 |
. . . . . . . . . . . . . . . . . 18
      ![[,] [,]](_icc.gif)   |
210 | 209 | sseli 3427 |
. . . . . . . . . . . . . . . . 17
       ![[,] [,]](_icc.gif)    |
211 | 210, 140 | sylan2 477 |
. . . . . . . . . . . . . . . 16
 
    
      |
212 | | nfcvd 2592 |
. . . . . . . . . . . . . . . . 17
         |
213 | | itgsubst.e |
. . . . . . . . . . . . . . . . 17
   |
214 | 212, 213 | csbiegf 3386 |
. . . . . . . . . . . . . . . 16
       ![]_ ]_](_urbrack.gif)   |
215 | 211, 214 | syl 17 |
. . . . . . . . . . . . . . 15
 
    
  ![]_ ]_](_urbrack.gif)   |
216 | 215 | oveq1d 6303 |
. . . . . . . . . . . . . 14
 
    
   ![]_ ]_](_urbrack.gif)      |
217 | 216 | itgeq2dv 22732 |
. . . . . . . . . . . . 13
          ![]_ ]_](_urbrack.gif)              |
218 | 3 | ditgpos 22804 |
. . . . . . . . . . . . 13
 _  ![] ]](rbrack.gif)    ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)
    |
219 | 3 | ditgpos 22804 |
. . . . . . . . . . . . 13
 _  ![] ]](rbrack.gif)               |
220 | 217, 218,
219 | 3eqtr4d 2494 |
. . . . . . . . . . . 12
 _  ![] ]](rbrack.gif)    ![]_ ]_](_urbrack.gif)   _  ![] ]](rbrack.gif)      |
221 | 208, 220 | syl5eqr 2498 |
. . . . . . . . . . 11
 _  ![] ]](rbrack.gif)     ![]_ ]_](_urbrack.gif)  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   _  ![] ]](rbrack.gif)      |
222 | 221 | adantr 467 |
. . . . . . . . . 10
 
     
        ![[,] [,]](_icc.gif)         _  ![] ]](rbrack.gif)     ![]_ ]_](_urbrack.gif)  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   _  ![] ]](rbrack.gif)      |
223 | 186, 200,
222 | 3eqtr3d 2492 |
. . . . . . . . 9
 
     
        ![[,] [,]](_icc.gif)         _  ![] ]](rbrack.gif)  _  ![] ]](rbrack.gif)      |
224 | 223 | expr 619 |
. . . . . . . 8
 
    
       
  ![[,] [,]](_icc.gif)       _
 ![] ]](rbrack.gif)  _  ![] ]](rbrack.gif)       |
225 | 146, 224 | sylbid 219 |
. . . . . . 7
 
    
       
  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          _  ![] ]](rbrack.gif)
 _  ![] ]](rbrack.gif)       |
226 | 129, 225 | sylbid 219 |
. . . . . 6
 
    
       
  ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       _
 ![] ]](rbrack.gif)  _  ![] ]](rbrack.gif)       |
227 | 117, 226 | syl5bir 222 |
. . . . 5
 
    
           ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)       _
 ![] ]](rbrack.gif)  _  ![] ]](rbrack.gif)       |
228 | 227 | rexlimdvva 2885 |
. . . 4
                  ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
   ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)       _
 ![] ]](rbrack.gif)  _  ![] ]](rbrack.gif)       |
229 | 116, 228 | syl5bi 221 |
. . 3
            ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)     
         ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)       _
 ![] ]](rbrack.gif)  _  ![] ]](rbrack.gif)       |
230 | 65, 113, 229 | syl2and 486 |
. 2
      ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)      
  ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)       _  ![] ]](rbrack.gif)
 _  ![] ]](rbrack.gif)       |
231 | 10, 230 | mpd 15 |
1
 _  ![] ]](rbrack.gif)  _  ![] ]](rbrack.gif)      |