Theorem rspc4v

Description: 4-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 7-Feb-2025)

	Ref	Expression
Hypotheses	rspc4v.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
	rspc4v.2	⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜃 ) )
	rspc4v.3	⊢ ( 𝑧 = 𝐶 → ( 𝜃 ↔ 𝜏 ) )
	rspc4v.4	⊢ ( 𝑤 = 𝐷 → ( 𝜏 ↔ 𝜓 ) )
Assertion	rspc4v	⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑈 ) ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑇 ∀ 𝑤 ∈ 𝑈 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		rspc4v.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
2		rspc4v.2	⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜃 ) )
3		rspc4v.3	⊢ ( 𝑧 = 𝐶 → ( 𝜃 ↔ 𝜏 ) )
4		rspc4v.4	⊢ ( 𝑤 = 𝐷 → ( 𝜏 ↔ 𝜓 ) )
5		df-3an	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝐶 ∈ 𝑇 ) )
6	1	ralbidv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑤 ∈ 𝑈 𝜑 ↔ ∀ 𝑤 ∈ 𝑈 𝜒 ) )
7	2	ralbidv	⊢ ( 𝑦 = 𝐵 → ( ∀ 𝑤 ∈ 𝑈 𝜒 ↔ ∀ 𝑤 ∈ 𝑈 𝜃 ) )
8	3	ralbidv	⊢ ( 𝑧 = 𝐶 → ( ∀ 𝑤 ∈ 𝑈 𝜃 ↔ ∀ 𝑤 ∈ 𝑈 𝜏 ) )
9	6 7 8	rspc3v	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑇 ∀ 𝑤 ∈ 𝑈 𝜑 → ∀ 𝑤 ∈ 𝑈 𝜏 ) )
10	4	rspcv	⊢ ( 𝐷 ∈ 𝑈 → ( ∀ 𝑤 ∈ 𝑈 𝜏 → 𝜓 ) )
11	9 10	sylan9	⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ 𝐷 ∈ 𝑈 ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑇 ∀ 𝑤 ∈ 𝑈 𝜑 → 𝜓 ) )
12	5 11	sylanbr	⊢ ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝐶 ∈ 𝑇 ) ∧ 𝐷 ∈ 𝑈 ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑇 ∀ 𝑤 ∈ 𝑈 𝜑 → 𝜓 ) )
13	12	anasss	⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑈 ) ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑇 ∀ 𝑤 ∈ 𝑈 𝜑 → 𝜓 ) )