Theorem nfald

Description: Deduction form of nfal . (Contributed by Mario Carneiro, 24-Sep-2016) (Proof shortened by Wolf Lammen, 16-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		nfald.1	$$⊢Ⅎy\phi$$
2		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	alimd	$$⊢\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$$