Step |
Hyp |
Ref |
Expression |
1 |
|
eumo |
|
2 |
1
|
imim2i |
|
3 |
|
moanimv |
|
4 |
2 3
|
sylibr |
|
5 |
4
|
2alimi |
|
6 |
|
funoprabg |
|
7 |
5 6
|
syl |
|
8 |
|
dmoprab |
|
9 |
|
nfa1 |
|
10 |
|
nfa2 |
|
11 |
|
simpl |
|
12 |
11
|
exlimiv |
|
13 |
|
euex |
|
14 |
13
|
imim2i |
|
15 |
14
|
ancld |
|
16 |
|
19.42v |
|
17 |
15 16
|
syl6ibr |
|
18 |
12 17
|
impbid2 |
|
19 |
18
|
sps |
|
20 |
19
|
sps |
|
21 |
9 10 20
|
opabbid |
|
22 |
8 21
|
eqtrid |
|
23 |
|
df-fn |
|
24 |
7 22 23
|
sylanbrc |
|