Metamath Proof Explorer


Theorem bj-nfimt

Description: Closed form of nfim and curried (exported) form of nfimt . (Contributed by BJ, 20-Oct-2021)

Ref Expression
Assertion bj-nfimt xφxψxφψ

Proof

Step Hyp Ref Expression
1 19.35 xφψxφxψ
2 id xφxφ
3 2 nfrd xφxφxφ
4 3 imim1d xφxφxψxφxψ
5 1 4 biimtrid xφxφψxφxψ
6 id xψxψ
7 6 nfrd xψxψxψ
8 7 imim2d xψxφxψxφxψ
9 19.38 xφxψxφψ
10 8 9 syl6 xψxφxψxφψ
11 5 10 syl9 xφxψxφψxφψ
12 df-nf xφψxφψxφψ
13 11 12 syl6ibr xφxψxφψ