Theorem bj-nfald

Description: Variant of nfald . (Contributed by BJ, 25-Dec-2023)

	Ref	Expression
Hypotheses	bj-nfald.1	|- ( ph -> A. y ph )
	bj-nfald.2	|- ( ph -> F/ x ps )
Assertion	bj-nfald	|- ( ph -> F/ x A. y ps )

Proof

Step	Hyp	Ref	Expression
1		bj-nfald.1	|- ( ph -> A. y ph )
2		bj-nfald.2	|- ( ph -> F/ x ps )
3		19.12	|- ( E. x A. y ps -> A. y E. x ps )
4	2	nfrd	|- ( ph -> ( E. x ps -> A. x ps ) )
5	1 4	alimdh	|- ( ph -> ( A. y E. x ps -> A. y A. x ps ) )
6		ax-11	|- ( A. y A. x ps -> A. x A. y ps )
7	3 5 6	syl56	|- ( ph -> ( E. x A. y ps -> A. x A. y ps ) )
8	7	nfd	|- ( ph -> F/ x A. y ps )