Step | Hyp | Ref
| Expression |
1 | | elpwi 3960 |
. . . 4
  
   |
2 | | fin12 8843 |
. . . . . . . . . . 11
 FinII |
3 | | fin23 8819 |
. . . . . . . . . . 11
 FinII FinIII |
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
 FinIII |
5 | | fin23 8819 |
. . . . . . . . . 10
   FinII   FinIII |
6 | 4, 5 | orim12i 519 |
. . . . . . . . 9
  

FinII 
FinIII
  FinIII  |
7 | 6 | ralimi 2781 |
. . . . . . . 8
 
   
FinII    FinIII   FinIII  |
8 | | fin1a2lem8 8837 |
. . . . . . . 8
     FinIII   FinIII
FinIII |
9 | 7, 8 | sylan2 477 |
. . . . . . 7
      
FinII
FinIII |
10 | 9 | adantr 467 |
. . . . . 6
     
  FinII  
 [ ]   
FinIII |
11 | | simplrl 770 |
. . . . . . . . . 10
      [ ]
   

     FinII     |
12 | | simprrr 775 |
. . . . . . . . . . 11
     [ ]
   [ ]   |
13 | 12 | adantr 467 |
. . . . . . . . . 10
      [ ]
   

     FinII  [ ]   |
14 | | simprl 764 |
. . . . . . . . . 10
      [ ]
   

     FinII     |
15 | | simplrl 770 |
. . . . . . . . . . . . . 14
      [ ]
    
   |
16 | | ssralv 3493 |
. . . . . . . . . . . . . 14
   
 
  FinII 
  
FinII   |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . 13
      [ ]
    
 
   
FinII 
   FinII   |
18 | | idd 25 |
. . . . . . . . . . . . . . 15
       [ ]           |
19 | | fin1a2lem13 8842 |
. . . . . . . . . . . . . . . . . . . . . . 23
    [ ]
  
 
  FinII |
20 | 19 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 [ ]  
 

  FinII  |
21 | 20 | 3expa 1208 |
. . . . . . . . . . . . . . . . . . . . 21
    [ ]

   
 

FinII  |
22 | 21 | adantlrl 726 |
. . . . . . . . . . . . . . . . . . . 20
     [ ]
     
   FinII  |
23 | 22 | adantll 720 |
. . . . . . . . . . . . . . . . . . 19
      [ ]
    
 

  FinII  |
24 | 23 | imp 431 |
. . . . . . . . . . . . . . . . . 18
       [ ]      
 
  FinII |
25 | 24 | ancom2s 811 |
. . . . . . . . . . . . . . . . 17
       [ ]      
 
  FinII |
26 | 25 | expr 620 |
. . . . . . . . . . . . . . . 16
       [ ]       
  FinII  |
27 | 26 | con4d 109 |
. . . . . . . . . . . . . . 15
       [ ]         
FinII    |
28 | 18, 27 | jaod 382 |
. . . . . . . . . . . . . 14
       [ ]          
FinII    |
29 | 28 | ralimdva 2796 |
. . . . . . . . . . . . 13
      [ ]
    
 
 

FinII 
   |
30 | 17, 29 | syld 45 |
. . . . . . . . . . . 12
      [ ]
    
 
   
FinII 
   |
31 | 30 | impr 625 |
. . . . . . . . . . 11
      [ ]
   

     FinII  
  |
32 | | dfss3 3422 |
. . . . . . . . . . 11

   |
33 | 31, 32 | sylibr 216 |
. . . . . . . . . 10
      [ ]
   

     FinII    |
34 | | simprrl 774 |
. . . . . . . . . . 11
     [ ]
     |
35 | 34 | adantr 467 |
. . . . . . . . . 10
      [ ]
   

     FinII    |
36 | | fin1a2lem12 8841 |
. . . . . . . . . 10
    [ ]
  
 
FinIII |
37 | 11, 13, 14, 33, 35, 36 | syl32anc 1276 |
. . . . . . . . 9
      [ ]
   

     FinII 
FinIII |
38 | 37 | expr 620 |
. . . . . . . 8
      [ ]
    
 
   
FinII
FinIII  |
39 | 38 | impancom 442 |
. . . . . . 7
      [ ]
       
FinII  
FinIII  |
40 | 39 | an32s 813 |
. . . . . 6
     
  FinII  
 [ ]     
FinIII  |
41 | 10, 40 | mt4d 144 |
. . . . 5
     
  FinII  
 [ ]    
  |
42 | 41 | exp32 610 |
. . . 4
      
FinII    
[ ] 
     |
43 | 1, 42 | syl5 33 |
. . 3
      
FinII   
  [ ] 
     |
44 | 43 | ralrimiv 2800 |
. 2
      
FinII 
   
[ ] 
    |
45 | | isfin2 8724 |
. . 3
 
FinII     
[ ] 
     |
46 | 45 | adantr 467 |
. 2
      
FinII  FinII
     [ ] 
     |
47 | 44, 46 | mpbird 236 |
1
      
FinII
FinII |