Theorem rspc3v

Description: 3-variable restricted specialization, using implicit substitution. (Contributed by NM, 10-May-2005)

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

Proof

Step	Hyp	Ref	Expression
1		rspc3v.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
2		rspc3v.2	⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜃 ) )
3		rspc3v.3	⊢ ( 𝑧 = 𝐶 → ( 𝜃 ↔ 𝜓 ) )
4	1	ralbidv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑧 ∈ 𝑇 𝜑 ↔ ∀ 𝑧 ∈ 𝑇 𝜒 ) )
5	2	ralbidv	⊢ ( 𝑦 = 𝐵 → ( ∀ 𝑧 ∈ 𝑇 𝜒 ↔ ∀ 𝑧 ∈ 𝑇 𝜃 ) )
6	4 5	rspc2v	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑇 𝜑 → ∀ 𝑧 ∈ 𝑇 𝜃 ) )
7	3	rspcv	⊢ ( 𝐶 ∈ 𝑇 → ( ∀ 𝑧 ∈ 𝑇 𝜃 → 𝜓 ) )
8	6 7	sylan9	⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝐶 ∈ 𝑇 ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑇 𝜑 → 𝜓 ) )
9	8	3impa	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑇 𝜑 → 𝜓 ) )