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	|- F/ x ph
	dvelimalcased.2	|- ( -. A. x x = y -> F/ z ph )
	dvelimalcased.3	|- ( ( ph /\ -. A. x x = y ) -> F/ x ps )
	dvelimalcased.4	|- ( ( ph /\ -. A. x x = y ) -> F/ z th )
	dvelimalcased.5	|- ( ( ph /\ -. A. x x = y ) -> ( z = x -> ( ps -> th ) ) )
	dvelimalcased.6	|- ( ( ph /\ A. x x = y ) -> ( ch -> th ) )
	dvelimalcased.7	|- ( ph -> A. z ps )
	dvelimalcased.8	|- ( ph -> A. x ch )
Assertion	dvelimalcased	|- ( ph -> A. x th )

Proof

Step	Hyp	Ref	Expression
1		dvelimalcased.1	|- F/ x ph
2		dvelimalcased.2	|- ( -. A. x x = y -> F/ z ph )
3		dvelimalcased.3	|- ( ( ph /\ -. A. x x = y ) -> F/ x ps )
4		dvelimalcased.4	|- ( ( ph /\ -. A. x x = y ) -> F/ z th )
5		dvelimalcased.5	|- ( ( ph /\ -. A. x x = y ) -> ( z = x -> ( ps -> th ) ) )
6		dvelimalcased.6	|- ( ( ph /\ A. x x = y ) -> ( ch -> th ) )
7		dvelimalcased.7	|- ( ph -> A. z ps )
8		dvelimalcased.8	|- ( ph -> A. x ch )
9		nfa1	|- F/ x A. x x = y
10	1 9	nfan	|- F/ x ( ph /\ A. x x = y )
11	10 6	alimd	|- ( ( ph /\ A. x x = y ) -> ( A. x ch -> A. x th ) )
12	11	ex	|- ( ph -> ( A. x x = y -> ( A. x ch -> A. x th ) ) )
13	8 12	mpid	|- ( ph -> ( A. x x = y -> A. x th ) )
14		nfv	|- F/ z -. A. x x = y
15	14 2	nfan1c	|- F/ z ( ph /\ -. A. x x = y )
16		nfna1	|- F/ x -. A. x x = y
17	1 16	nfan	|- F/ x ( ph /\ -. A. x x = y )
18	15 17 3 4 5	cbv1v	|- ( ( ph /\ -. A. x x = y ) -> ( A. z ps -> A. x th ) )
19	18	ex	|- ( ph -> ( -. A. x x = y -> ( A. z ps -> A. x th ) ) )
20	7 19	mpid	|- ( ph -> ( -. A. x x = y -> A. x th ) )
21	13 20	pm2.61d	|- ( ph -> A. x th )