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	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜑 )
	dvelimalcasei.2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑧 𝜒 )
	dvelimalcasei.3	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑥 → ( 𝜑 → 𝜒 ) ) )
	dvelimalcasei.4	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜓 → 𝜒 ) )
	dvelimalcasei.5	⊢ ∀ 𝑧 𝜑
	dvelimalcasei.6	⊢ ∀ 𝑥 𝜓
Assertion	dvelimalcasei	⊢ ∀ 𝑥 𝜒

Proof

Step	Hyp	Ref	Expression
1		dvelimalcasei.1	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜑 )
2		dvelimalcasei.2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑧 𝜒 )
3		dvelimalcasei.3	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑥 → ( 𝜑 → 𝜒 ) ) )
4		dvelimalcasei.4	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜓 → 𝜒 ) )
5		dvelimalcasei.5	⊢ ∀ 𝑧 𝜑
6		dvelimalcasei.6	⊢ ∀ 𝑥 𝜓
7		nftru	⊢ Ⅎ 𝑥 ⊤
8		nfvd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑧 ⊤ )
9	1	adantl	⊢ ( ( ⊤ ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜑 )
10	2	adantl	⊢ ( ( ⊤ ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑧 𝜒 )
11	3	adantl	⊢ ( ( ⊤ ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝑧 = 𝑥 → ( 𝜑 → 𝜒 ) ) )
12	4	adantl	⊢ ( ( ⊤ ∧ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝜓 → 𝜒 ) )
13	5	a1i	⊢ ( ⊤ → ∀ 𝑧 𝜑 )
14	6	a1i	⊢ ( ⊤ → ∀ 𝑥 𝜓 )
15	7 8 9 10 11 12 13 14	dvelimalcased	⊢ ( ⊤ → ∀ 𝑥 𝜒 )
16	15	mptru	⊢ ∀ 𝑥 𝜒