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	Could not format assertion : No typesetting found for |- F/ x AE y ( ph -> ps ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		nfals.1	$$⊢Ⅎx\phi$$
2		nfals.2	$$⊢Ⅎx\psi$$
3		df-als	Could not format ( AE y ( ph -> ps ) <-> ( A. y ( ph -> ps ) /\ E. y ph ) ) : No typesetting found for |- ( AE y ( ph -> ps ) <-> ( A. y ( ph -> ps ) /\ E. y ph ) ) with typecode |-
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	Could not format F/ x AE y ( ph -> ps ) : No typesetting found for |- F/ x AE y ( ph -> ps ) with typecode |-