Theorem dvelimalcasei

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

	Ref	Expression
Hypotheses	dvelimalcasei.1	|- ( -. A. x x = y -> F/ x ph )
	dvelimalcasei.2	|- ( -. A. x x = y -> F/ z ch )
	dvelimalcasei.3	|- ( -. A. x x = y -> ( z = x -> ( ph -> ch ) ) )
	dvelimalcasei.4	|- ( A. x x = y -> ( ps -> ch ) )
	dvelimalcasei.5	|- A. z ph
	dvelimalcasei.6	|- A. x ps
Assertion	dvelimalcasei	|- A. x ch

Proof

Step	Hyp	Ref	Expression
1		dvelimalcasei.1	|- ( -. A. x x = y -> F/ x ph )
2		dvelimalcasei.2	|- ( -. A. x x = y -> F/ z ch )
3		dvelimalcasei.3	|- ( -. A. x x = y -> ( z = x -> ( ph -> ch ) ) )
4		dvelimalcasei.4	|- ( A. x x = y -> ( ps -> ch ) )
5		dvelimalcasei.5	|- A. z ph
6		dvelimalcasei.6	|- A. x ps
7		nftru	|- F/ x T.
8		nfvd	|- ( -. A. x x = y -> F/ z T. )
9	1	adantl	|- ( ( T. /\ -. A. x x = y ) -> F/ x ph )
10	2	adantl	|- ( ( T. /\ -. A. x x = y ) -> F/ z ch )
11	3	adantl	|- ( ( T. /\ -. A. x x = y ) -> ( z = x -> ( ph -> ch ) ) )
12	4	adantl	|- ( ( T. /\ A. x x = y ) -> ( ps -> ch ) )
13	5	a1i	|- ( T. -> A. z ph )
14	6	a1i	|- ( T. -> A. x ps )
15	7 8 9 10 11 12 13 14	dvelimalcased	|- ( T. -> A. x ch )
16	15	mptru	|- A. x ch