Metamath Proof Explorer


Theorem bj-nfdt0

Description: A theorem close to a closed form of nf5d and nf5dh . (Contributed by BJ, 2-May-2019)

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

Proof

Step Hyp Ref Expression
1 alim xφψxψxφxψxψ
2 nf5 xψxψxψ
3 1 2 imbitrrdi xφψxψxφxψ