Theorem rspc3dv

Description: 3-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2025)

	Ref	Expression
Hypotheses	rspc3dv.1	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜃 ) )
	rspc3dv.2	⊢ ( 𝑦 = 𝐵 → ( 𝜃 ↔ 𝜏 ) )
	rspc3dv.3	⊢ ( 𝑧 = 𝐶 → ( 𝜏 ↔ 𝜒 ) )
	rspc3dv.4	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐸 ∀ 𝑧 ∈ 𝐹 𝜓 )
	rspc3dv.5	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
	rspc3dv.6	⊢ ( 𝜑 → 𝐵 ∈ 𝐸 )
	rspc3dv.7	⊢ ( 𝜑 → 𝐶 ∈ 𝐹 )
Assertion	rspc3dv	⊢ ( 𝜑 → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		rspc3dv.1	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜃 ) )
2		rspc3dv.2	⊢ ( 𝑦 = 𝐵 → ( 𝜃 ↔ 𝜏 ) )
3		rspc3dv.3	⊢ ( 𝑧 = 𝐶 → ( 𝜏 ↔ 𝜒 ) )
4		rspc3dv.4	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐸 ∀ 𝑧 ∈ 𝐹 𝜓 )
5		rspc3dv.5	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
6		rspc3dv.6	⊢ ( 𝜑 → 𝐵 ∈ 𝐸 )
7		rspc3dv.7	⊢ ( 𝜑 → 𝐶 ∈ 𝐹 )
8	5 6 7	3jca	⊢ ( 𝜑 → ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐸 ∧ 𝐶 ∈ 𝐹 ) )
9	1 2 3	rspc3v	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐸 ∧ 𝐶 ∈ 𝐹 ) → ( ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐸 ∀ 𝑧 ∈ 𝐹 𝜓 → 𝜒 ) )
10	8 4 9	sylc	⊢ ( 𝜑 → 𝜒 )