Step | Hyp | Ref
| Expression |
1 | | 19.26 1740 |
. . 3
    
 
    |
2 | | equid 1863 |
. . . . . . . 8
 |
3 | 2 | a1i 11 |
. . . . . . 7
   |
4 | 3 | ax-gen 1677 |
. . . . . 6
     |
5 | 4 | a1i 11 |
. . . . 5
       |
6 | | equequ1 1875 |
. . . . . . . . 9
 
   |
7 | | equequ2 1876 |
. . . . . . . . 9
 
   |
8 | 6, 7 | sylan9bb 714 |
. . . . . . . 8
 
     |
9 | 8 | sps-o 32543 |
. . . . . . 7
     
   |
10 | | nfa1-o 32550 |
. . . . . . . 8
       |
11 | 9 | imbi2d 323 |
. . . . . . . 8
        
    |
12 | 10, 11 | albid 1983 |
. . . . . . 7
        

       |
13 | 9, 12 | imbi12d 327 |
. . . . . 6
           

        |
14 | 13 | adantr 472 |
. . . . 5
           
    

        |
15 | 5, 14 | mpbii 216 |
. . . 4
                  |
16 | 15 | exp32 616 |
. . 3
      

          |
17 | 1, 16 | sylbir 218 |
. 2
   
  
           |
18 | | equequ1 1875 |
. . . . . . 7
 
   |
19 | 18 | ad2antll 743 |
. . . . . 6
           |
20 | | axc9 2154 |
. . . . . . . . 9
 
  

    |
21 | 20 | impcom 437 |
. . . . . . . 8
    


   |
22 | 21 | adantrr 731 |
. . . . . . 7
            |
23 | | equtrr 1874 |
. . . . . . . 8
 
   |
24 | 23 | alimi 1692 |
. . . . . . 7
 
      |
25 | 22, 24 | syl6 33 |
. . . . . 6
               |
26 | 19, 25 | sylbid 223 |
. . . . 5
               |
27 | 26 | adantll 728 |
. . . 4
                  |
28 | | equequ1 1875 |
. . . . . . 7
 
   |
29 | 28 | sps-o 32543 |
. . . . . 6
 
    |
30 | 29 | imbi2d 323 |
. . . . . . 7
 
 


    |
31 | 30 | dral2-o 32565 |
. . . . . 6
 
   
   
    |
32 | 29, 31 | imbi12d 327 |
. . . . 5
 
 
    

        |
33 | 32 | ad2antrr 740 |
. . . 4
           
    

        |
34 | 27, 33 | mpbid 215 |
. . 3
                  |
35 | 34 | exp32 616 |
. 2
   

  

         |
36 | | equequ2 1876 |
. . . . . . 7
 
   |
37 | 36 | ad2antll 743 |
. . . . . 6
           |
38 | | axc9 2154 |
. . . . . . . . 9
 
  

    |
39 | 38 | imp 436 |
. . . . . . . 8
    


   |
40 | 39 | adantrr 731 |
. . . . . . 7
            |
41 | 36 | biimprcd 233 |
. . . . . . . 8
     |
42 | 41 | alimi 1692 |
. . . . . . 7
 
      |
43 | 40, 42 | syl6 33 |
. . . . . 6
               |
44 | 37, 43 | sylbid 223 |
. . . . 5
               |
45 | 44 | adantlr 729 |
. . . 4
   
              |
46 | 7 | sps-o 32543 |
. . . . . 6
 
    |
47 | 46 | imbi2d 323 |
. . . . . . 7
 
 


    |
48 | 47 | dral2-o 32565 |
. . . . . 6
 
       
    |
49 | 46, 48 | imbi12d 327 |
. . . . 5
 
 
    

        |
50 | 49 | ad2antlr 741 |
. . . 4
   
       
    

        |
51 | 45, 50 | mpbid 215 |
. . 3
   
              |
52 | 51 | exp32 616 |
. 2
   

  

         |
53 | | ax6ev 1815 |
. . . . 5

 |
54 | | ax6ev 1815 |
. . . . . . 7
  |
55 | | ax-1 6 |
. . . . . . . . . . 11
     |
56 | 55 | alrimiv 1781 |
. . . . . . . . . 10
       |
57 | | equequ1 1875 |
. . . . . . . . . . . . 13
 
   |
58 | | equequ2 1876 |
. . . . . . . . . . . . 13
 
   |
59 | 57, 58 | sylan9bb 714 |
. . . . . . . . . . . 12
 
     |
60 | 59 | adantl 473 |
. . . . . . . . . . 11
   
  
 

   |
61 | | dveeq2-o 32568 |
. . . . . . . . . . . . . . 15
 


   |
62 | | dveeq2-o 32568 |
. . . . . . . . . . . . . . 15
 


   |
63 | 61, 62 | im2anan9 853 |
. . . . . . . . . . . . . 14
    
 
   
    |
64 | 63 | imp 436 |
. . . . . . . . . . . . 13
   
  
 
 
    |
65 | | 19.26 1740 |
. . . . . . . . . . . . 13
    
 
    |
66 | 64, 65 | sylibr 217 |
. . . . . . . . . . . 12
   
  
 
      |
67 | | nfa1-o 32550 |
. . . . . . . . . . . . 13
       |
68 | 59 | sps-o 32543 |
. . . . . . . . . . . . . 14
     
   |
69 | 68 | imbi2d 323 |
. . . . . . . . . . . . 13
        
    |
70 | 67, 69 | albid 1983 |
. . . . . . . . . . . 12
        

       |
71 | 66, 70 | syl 17 |
. . . . . . . . . . 11
   
  
 
   

       |
72 | 60, 71 | imbi12d 327 |
. . . . . . . . . 10
   
  
 
    
 

        |
73 | 56, 72 | mpbii 216 |
. . . . . . . . 9
   
  
 

       |
74 | 73 | exp32 616 |
. . . . . . . 8
    

    
      |
75 | 74 | exlimdv 1787 |
. . . . . . 7
    
 
 
         |
76 | 54, 75 | mpi 20 |
. . . . . 6
    

         |
77 | 76 | exlimdv 1787 |
. . . . 5
    
 
         |
78 | 53, 77 | mpi 20 |
. . . 4
    

       |
79 | 78 | a1d 25 |
. . 3
    

         |
80 | 79 | a1d 25 |
. 2
    
  

         |
81 | 17, 35, 52, 80 | 4cases 964 |
1
 

         |