Theorem dvelimalcasei

Description: Eliminate a disjoint variable condition from a universally quantified statement using cases. Inference form of dvelimalcased . See axsepg2 for an example of its use. (Contributed by BTernaryTau, 31-Jul-2025)

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

Proof

Step	Hyp	Ref	Expression
1		dvelimalcasei.1	$$⊢\neg \forall xx=y\to Ⅎx\phi$$
2		dvelimalcasei.2	$$⊢\neg \forall xx=y\to Ⅎz\chi$$
3		dvelimalcasei.3	$$⊢\neg \forall xx=y\to \left(z=x\to \left(\phi \to \chi \right)\right)$$
4		dvelimalcasei.4	$$⊢\forall xx=y\to \left(\psi \to \chi \right)$$
5		dvelimalcasei.5	$$⊢\forall z\phi$$
6		dvelimalcasei.6	$$⊢\forall x\psi$$
7		nftru	$$⊢Ⅎx\top$$
8		nfvd	$$⊢\neg \forall xx=y\to Ⅎz\top$$
9	1	adantl	$$⊢\left(\top \wedge \neg \forall xx=y\right)\to Ⅎx\phi$$
10	2	adantl	$$⊢\left(\top \wedge \neg \forall xx=y\right)\to Ⅎz\chi$$
11	3	adantl	$$⊢\left(\top \wedge \neg \forall xx=y\right)\to \left(z=x\to \left(\phi \to \chi \right)\right)$$
12	4	adantl	$$⊢\left(\top \wedge \forall xx=y\right)\to \left(\psi \to \chi \right)$$
13	5	a1i	$$⊢\top \to \forall z\phi$$
14	6	a1i	$$⊢\top \to \forall x\psi$$
15	7 8 9 10 11 12 13 14	dvelimalcased	$$⊢\top \to \forall x\chi$$
16	15	mptru	$$⊢\forall x\chi$$