Theorem bj-nfald

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

	Ref	Expression
Hypotheses	bj-nfald.1	$$⊢\phi \to \forall y\phi$$
	bj-nfald.2	$$⊢\phi \to Ⅎx\psi$$
Assertion	bj-nfald	$$⊢\phi \to Ⅎx\forall y\psi$$

Proof

Step	Hyp	Ref	Expression
1		bj-nfald.1	$$⊢\phi \to \forall y\phi$$
2		bj-nfald.2	$$⊢\phi \to Ⅎx\psi$$
3		19.12	$$⊢\exists x\forall y\psi \to \forall y\exists x\psi$$
4	2	nfrd	$$⊢\phi \to \left(\exists x\psi \to \forall x\psi \right)$$
5	1 4	alimdh	$$⊢\phi \to \left(\forall y\exists x\psi \to \forall y\forall x\psi \right)$$
6		ax-11	$$⊢\forall y\forall x\psi \to \forall x\forall y\psi$$
7	3 5 6	syl56	$$⊢\phi \to \left(\exists x\forall y\psi \to \forall x\forall y\psi \right)$$
8	7	nfd	$$⊢\phi \to Ⅎx\forall y\psi$$