Theorem bj-nexdt

Description: Closed form of nexd . (Contributed by BJ, 20-Oct-2019)

	Ref	Expression
Assertion	bj-nexdt	|- ( F/ x ph -> ( A. x ( ph -> -. ps ) -> ( ph -> -. E. x ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		nf5r	|- ( F/ x ph -> ( ph -> A. x ph ) )
2		bj-nexdh	|- ( A. x ( ph -> -. ps ) -> ( ( ph -> A. x ph ) -> ( ph -> -. E. x ps ) ) )
3	1 2	syl5com	|- ( F/ x ph -> ( A. x ( ph -> -. ps ) -> ( ph -> -. E. x ps ) ) )