Step | Hyp | Ref
| Expression |
1 | | djulf1o 7057 |
. . . . . . . . 9
inl        |
2 | | f1of1 5461 |
. . . . . . . . 9
inl       inl     
   |
3 | 1, 2 | ax-mp 5 |
. . . . . . . 8
inl        |
4 | | ssv 3178 |
. . . . . . . 8
 |
5 | | f1ores 5477 |
. . . . . . . 8
 inl     

 inl      inl    |
6 | 3, 4, 5 | mp2an 426 |
. . . . . . 7
inl      inl   |
7 | | f1oeng 6757 |
. . . . . . 7
  inl      inl  
inl    |
8 | 6, 7 | mpan2 425 |
. . . . . 6
 inl    |
9 | 8 | ensymd 6783 |
. . . . 5
 inl    |
10 | | djurf1o 7058 |
. . . . . . . 8
inr        |
11 | | f1of1 5461 |
. . . . . . . 8
inr      
inr         |
12 | 10, 11 | ax-mp 5 |
. . . . . . 7
inr        |
13 | | f1ores 5477 |
. . . . . . 7
 inr        inr      inr    |
14 | 12, 4, 13 | mp2an 426 |
. . . . . 6
inr      inr   |
15 | | f1oeng 6757 |
. . . . . 6
  inr      inr  
inr    |
16 | 14, 15 | mpan2 425 |
. . . . 5
 inr    |
17 | | entr 6784 |
. . . . 5
  inl  inr  
inl 
inr    |
18 | 9, 16, 17 | syl2anc 411 |
. . . 4
 inl  inr    |
19 | 18 | adantr 276 |
. . 3
 
 inl  inr    |
20 | | ssv 3178 |
. . . . . . . 8
 |
21 | | f1ores 5477 |
. . . . . . . 8
 inr        inr      inr    |
22 | 12, 20, 21 | mp2an 426 |
. . . . . . 7
inr      inr   |
23 | | f1oeng 6757 |
. . . . . . 7
  inr      inr  
inr    |
24 | 22, 23 | mpan2 425 |
. . . . . 6
 inr    |
25 | 24 | adantl 277 |
. . . . 5
 
 inr    |
26 | 25 | ensymd 6783 |
. . . 4
 
 inr    |
27 | | f1ores 5477 |
. . . . . . 7
 inl     

 inl      inl    |
28 | 3, 20, 27 | mp2an 426 |
. . . . . 6
inl      inl   |
29 | | f1oeng 6757 |
. . . . . 6
  inl      inl  
inl    |
30 | 28, 29 | mpan2 425 |
. . . . 5
 inl    |
31 | 30 | adantl 277 |
. . . 4
 
 inl    |
32 | | entr 6784 |
. . . 4
  inr  inl  
inr 
inl    |
33 | 26, 31, 32 | syl2anc 411 |
. . 3
 
 inr  inl    |
34 | | djuin 7063 |
. . . 4
 inl  inr    |
35 | 34 | a1i 9 |
. . 3
 
  inl 
inr     |
36 | | incom 3328 |
. . . . 5
 inl  inr    inr 
inl    |
37 | | djuin 7063 |
. . . . 5
 inl  inr    |
38 | 36, 37 | eqtr3i 2200 |
. . . 4
 inr  inl    |
39 | 38 | a1i 9 |
. . 3
 
  inr 
inl     |
40 | | unen 6816 |
. . 3
   inl 
inr 
inr 
inl     inl 
inr    inr 
inl      inl  inr    inr  inl     |
41 | 19, 33, 35, 39, 40 | syl22anc 1239 |
. 2
 
  inl  inr    inr  inl     |
42 | | djuun 7066 |
. 2
 inl  inr    ⊔
  |
43 | | uncom 3280 |
. . 3
 inr  inl    inl  inr    |
44 | | djuun 7066 |
. . 3
 inl  inr    ⊔
  |
45 | 43, 44 | eqtri 2198 |
. 2
 inr  inl    ⊔
  |
46 | 41, 42, 45 | 3brtr3g 4037 |
1
 
  ⊔
  ⊔
   |