This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑇 𝜑 → 𝜓 ) )