Theorem dvelimalcased

Description: Eliminate a disjoint variable condition from a universally quantified statement using cases. (Contributed by BTernaryTau, 31-Jul-2025)

	Ref	Expression
Hypotheses	dvelimalcased.1	$$⊢Ⅎx\phi$$
	dvelimalcased.2	$$⊢\neg \forall xx=y\to Ⅎz\phi$$
	dvelimalcased.3	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to Ⅎx\psi$$
	dvelimalcased.4	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to Ⅎz\theta$$
	dvelimalcased.5	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to \left(z=x\to \left(\psi \to \theta \right)\right)$$
	dvelimalcased.6	$$⊢\left(\phi \wedge \forall xx=y\right)\to \left(\chi \to \theta \right)$$
	dvelimalcased.7	$$⊢\phi \to \forall z\psi$$
	dvelimalcased.8	$$⊢\phi \to \forall x\chi$$
Assertion	dvelimalcased	$$⊢\phi \to \forall x\theta$$

Proof

Step	Hyp	Ref	Expression
1		dvelimalcased.1	$$⊢Ⅎx\phi$$
2		dvelimalcased.2	$$⊢\neg \forall xx=y\to Ⅎz\phi$$
3		dvelimalcased.3	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to Ⅎx\psi$$
4		dvelimalcased.4	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to Ⅎz\theta$$
5		dvelimalcased.5	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to \left(z=x\to \left(\psi \to \theta \right)\right)$$
6		dvelimalcased.6	$$⊢\left(\phi \wedge \forall xx=y\right)\to \left(\chi \to \theta \right)$$
7		dvelimalcased.7	$$⊢\phi \to \forall z\psi$$
8		dvelimalcased.8	$$⊢\phi \to \forall x\chi$$
9		nfa1	$$⊢Ⅎx\forall xx=y$$
10	1 9	nfan	$$⊢Ⅎx\left(\phi \wedge \forall xx=y\right)$$
11	10 6	alimd	$$⊢\left(\phi \wedge \forall xx=y\right)\to \left(\forall x\chi \to \forall x\theta \right)$$
12	11	ex	$$⊢\phi \to \left(\forall xx=y\to \left(\forall x\chi \to \forall x\theta \right)\right)$$
13	8 12	mpid	$$⊢\phi \to \left(\forall xx=y\to \forall x\theta \right)$$
14		nfv	$$⊢Ⅎz\neg \forall xx=y$$
15	14 2	nfan1c	$$⊢Ⅎz\left(\phi \wedge \neg \forall xx=y\right)$$
16		nfna1	$$⊢Ⅎx\neg \forall xx=y$$
17	1 16	nfan	$$⊢Ⅎx\left(\phi \wedge \neg \forall xx=y\right)$$
18	15 17 3 4 5	cbv1v	$$⊢\left(\phi \wedge \neg \forall xx=y\right)\to \left(\forall z\psi \to \forall x\theta \right)$$
19	18	ex	$$⊢\phi \to \left(\neg \forall xx=y\to \left(\forall z\psi \to \forall x\theta \right)\right)$$
20	7 19	mpid	$$⊢\phi \to \left(\neg \forall xx=y\to \forall x\theta \right)$$
21	13 20	pm2.61d	$$⊢\phi \to \forall x\theta$$