Theorem nfals

Description: Bound-variable hypothesis builder for "all some". (Contributed by David A. Wheeler, 12-Jul-2026)

	Ref	Expression
Hypotheses	nfals.1	$$⊢Ⅎx\phi$$
	nfals.2	$$⊢Ⅎx\psi$$
Assertion	nfals	$$⊢Ⅎx\forall \exists y\left(\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfals.1	$$⊢Ⅎx\phi$$
2		nfals.2	$$⊢Ⅎx\psi$$
3		df-als	$$⊢\forall \exists y\left(\phi \to \psi \right)\leftrightarrow \left(\forall y\left(\phi \to \psi \right)\wedge \exists y\phi \right)$$
4	1 2	nfim	$$⊢Ⅎx\left(\phi \to \psi \right)$$
5	4	nfal	$$⊢Ⅎx\forall y\left(\phi \to \psi \right)$$
6	1	nfex	$$⊢Ⅎx\exists y\phi$$
7	5 6	nfan	$$⊢Ⅎx\left(\forall y\left(\phi \to \psi \right)\wedge \exists y\phi \right)$$
8	3 7	nfxfr	$$⊢Ⅎx\forall \exists y\left(\phi \to \psi \right)$$