Step | Hyp | Ref
| Expression |
1 | | ellines 30969 |
. . 3
 LinesEE              
 Line    |
2 | | simpll1 1053 |
. . . . . . . . . . . 12
       
         Line
 Line      |
3 | | simpll2 1054 |
. . . . . . . . . . . 12
       
         Line
 Line          |
4 | | simpll3 1055 |
. . . . . . . . . . . 12
       
         Line
 Line          |
5 | | simplr 767 |
. . . . . . . . . . . 12
       
         Line
 Line      |
6 | | liness 30962 |
. . . . . . . . . . . 12
              Line       |
7 | 2, 3, 4, 5, 6 | syl13anc 1278 |
. . . . . . . . . . 11
       
         Line
 Line     Line
      |
8 | | simprll 777 |
. . . . . . . . . . 11
       
         Line
 Line     Line   |
9 | 7, 8 | sseldd 3445 |
. . . . . . . . . 10
       
         Line
 Line          |
10 | | simprlr 778 |
. . . . . . . . . . 11
       
         Line
 Line     Line   |
11 | 7, 10 | sseldd 3445 |
. . . . . . . . . 10
       
         Line
 Line          |
12 | | simplll 773 |
. . . . . . . . . . . . . . . 16
     Line  Line  
    
       Line   |
13 | 12 | adantl 472 |
. . . . . . . . . . . . . . 15
       
          Line  Line  
    
      
 Line   |
14 | | simpll1 1053 |
. . . . . . . . . . . . . . . 16
       
          Line  Line  
    
      
  |
15 | | simpll2 1054 |
. . . . . . . . . . . . . . . 16
       
          Line  Line  
    
             |
16 | | simpll3 1055 |
. . . . . . . . . . . . . . . 16
       
          Line  Line  
    
             |
17 | | simplr 767 |
. . . . . . . . . . . . . . . 16
       
          Line  Line  
    
         |
18 | | simprrl 779 |
. . . . . . . . . . . . . . . 16
       
          Line  Line  
    
      
      |
19 | | simprlr 778 |
. . . . . . . . . . . . . . . . 17
       
          Line  Line  
    
         |
20 | 19 | necomd 2691 |
. . . . . . . . . . . . . . . 16
       
          Line  Line  
    
         |
21 | | lineelsb2 30965 |
. . . . . . . . . . . . . . . 16
           
    
  
 Line  Line  Line    |
22 | 14, 15, 16, 17, 18, 20, 21 | syl132anc 1294 |
. . . . . . . . . . . . . . 15
       
          Line  Line  
    
         Line  Line  Line    |
23 | 13, 22 | mpd 15 |
. . . . . . . . . . . . . 14
       
          Line  Line  
    
        Line  Line   |
24 | | linecom 30967 |
. . . . . . . . . . . . . . 15
              Line  Line   |
25 | 14, 15, 18, 20, 24 | syl13anc 1278 |
. . . . . . . . . . . . . 14
       
          Line  Line  
    
        Line  Line   |
26 | 23, 25 | eqtrd 2496 |
. . . . . . . . . . . . 13
       
          Line  Line  
    
        Line  Line   |
27 | | neeq2 2699 |
. . . . . . . . . . . . . . . . 17
 
   |
28 | 27 | anbi2d 715 |
. . . . . . . . . . . . . . . 16
     Line  Line      Line  Line      |
29 | 28 | anbi1d 716 |
. . . . . . . . . . . . . . 15
      Line  Line   
         
    Line
 Line   
   
         |
30 | 29 | anbi2d 715 |
. . . . . . . . . . . . . 14
        
          Line  Line  
    
      
      
          Line  Line   
              |
31 | | oveq2 6328 |
. . . . . . . . . . . . . . 15
  Line  Line   |
32 | 31 | eqeq2d 2472 |
. . . . . . . . . . . . . 14
   Line  Line  Line  Line    |
33 | 30, 32 | imbi12d 326 |
. . . . . . . . . . . . 13
     
              Line  Line  
    
        Line  Line 
       
          Line  Line  
    
        Line  Line     |
34 | 26, 33 | mpbiri 241 |
. . . . . . . . . . . 12
        
          Line  Line  
    
        Line  Line    |
35 | | simp1 1014 |
. . . . . . . . . . . . . . . . . 18
       
          Line  Line  
    
            
        |
36 | | simp2l 1040 |
. . . . . . . . . . . . . . . . . 18
       
          Line  Line  
    
          Line
 Line     |
37 | 35, 36, 10 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
       
          Line  Line  
    
        Line   |
38 | | simp1l1 1107 |
. . . . . . . . . . . . . . . . . 18
       
          Line  Line  
    
         |
39 | | simp1l2 1108 |
. . . . . . . . . . . . . . . . . 18
       
          Line  Line  
    
             |
40 | | simp1l3 1109 |
. . . . . . . . . . . . . . . . . 18
       
          Line  Line  
    
             |
41 | | simp1r 1039 |
. . . . . . . . . . . . . . . . . 18
       
          Line  Line  
    
         |
42 | | simp2rr 1084 |
. . . . . . . . . . . . . . . . . 18
       
          Line  Line  
    
             |
43 | | simp3 1016 |
. . . . . . . . . . . . . . . . . . 19
       
          Line  Line  
    
         |
44 | 43 | necomd 2691 |
. . . . . . . . . . . . . . . . . 18
       
          Line  Line  
    
         |
45 | | lineelsb2 30965 |
. . . . . . . . . . . . . . . . . 18
           
    
  
 Line  Line  Line    |
46 | 38, 39, 40, 41, 42, 44, 45 | syl132anc 1294 |
. . . . . . . . . . . . . . . . 17
       
          Line  Line  
    
       
 Line  Line  Line    |
47 | 37, 46 | mpd 15 |
. . . . . . . . . . . . . . . 16
       
          Line  Line  
    
        Line  Line   |
48 | | linecom 30967 |
. . . . . . . . . . . . . . . . 17
              Line  Line   |
49 | 38, 39, 42, 44, 48 | syl13anc 1278 |
. . . . . . . . . . . . . . . 16
       
          Line  Line  
    
        Line  Line   |
50 | 47, 49 | eqtrd 2496 |
. . . . . . . . . . . . . . 15
       
          Line  Line  
    
        Line  Line   |
51 | 36 | simplld 766 |
. . . . . . . . . . . . . . . . 17
       
          Line  Line  
    
        Line   |
52 | 51, 50 | eleqtrd 2542 |
. . . . . . . . . . . . . . . 16
       
          Line  Line  
    
        Line   |
53 | | simp2rl 1083 |
. . . . . . . . . . . . . . . . 17
       
          Line  Line  
    
             |
54 | | simp2lr 1082 |
. . . . . . . . . . . . . . . . . 18
       
          Line  Line  
    
         |
55 | 54 | necomd 2691 |
. . . . . . . . . . . . . . . . 17
       
          Line  Line  
    
         |
56 | | lineelsb2 30965 |
. . . . . . . . . . . . . . . . 17
  
   
     
        Line  Line  Line    |
57 | 38, 42, 39, 43, 53, 55, 56 | syl132anc 1294 |
. . . . . . . . . . . . . . . 16
       
          Line  Line  
    
       
 Line  Line  Line    |
58 | 52, 57 | mpd 15 |
. . . . . . . . . . . . . . 15
       
          Line  Line  
    
        Line  Line   |
59 | | linecom 30967 |
. . . . . . . . . . . . . . . 16
  
   
       Line  Line   |
60 | 38, 42, 53, 55, 59 | syl13anc 1278 |
. . . . . . . . . . . . . . 15
       
          Line  Line  
    
        Line  Line   |
61 | 50, 58, 60 | 3eqtrd 2500 |
. . . . . . . . . . . . . 14
       
          Line  Line  
    
        Line  Line   |
62 | 61 | 3expa 1215 |
. . . . . . . . . . . . 13
        
          Line  Line  
    
         Line  Line   |
63 | 62 | expcom 441 |
. . . . . . . . . . . 12
        
          Line  Line  
    
        Line  Line    |
64 | 34, 63 | pm2.61ine 2719 |
. . . . . . . . . . 11
       
          Line  Line  
    
        Line  Line   |
65 | 64 | expr 624 |
. . . . . . . . . 10
       
         Line
 Line                Line  Line    |
66 | 9, 11, 65 | mp2and 690 |
. . . . . . . . 9
       
         Line
 Line     Line  Line   |
67 | 66 | ex 440 |
. . . . . . . 8
      
          Line  Line    Line  Line    |
68 | | eleq2 2529 |
. . . . . . . . . . 11
  Line

 Line    |
69 | | eleq2 2529 |
. . . . . . . . . . 11
  Line

 Line    |
70 | 68, 69 | anbi12d 722 |
. . . . . . . . . 10
  Line
 
   Line  Line     |
71 | 70 | anbi1d 716 |
. . . . . . . . 9
  Line
  

    Line  Line      |
72 | | eqeq1 2466 |
. . . . . . . . 9
  Line
  Line  Line  Line    |
73 | 71, 72 | imbi12d 326 |
. . . . . . . 8
  Line
       Line 
    Line
 Line    Line  Line     |
74 | 67, 73 | syl5ibrcom 230 |
. . . . . . 7
      
        Line       Line     |
75 | 74 | expimpd 612 |
. . . . . 6
 
          
 Line    


 Line     |
76 | 75 | 3expa 1215 |
. . . . 5
            
 
 Line        Line     |
77 | 76 | rexlimdva 2891 |
. . . 4
 
              Line 
  


 Line     |
78 | 77 | rexlimivv 2896 |
. . 3
  
             Line 
  


 Line    |
79 | 1, 78 | sylbi 200 |
. 2
 LinesEE   


 Line    |
80 | 79 | 3impib 1213 |
1
  LinesEE



 Line   |