Description: Closed form of nfim and curried (exported) form of nfimt . (Contributed by BJ, 20-Oct-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-nfimt | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.35 | |
|
2 | id | |
|
3 | 2 | nfrd | |
4 | 3 | imim1d | |
5 | 1 4 | biimtrid | |
6 | id | |
|
7 | 6 | nfrd | |
8 | 7 | imim2d | |
9 | 19.38 | |
|
10 | 8 9 | syl6 | |
11 | 5 10 | syl9 | |
12 | df-nf | |
|
13 | 11 12 | syl6ibr | |