Metamath Proof Explorer

Theorem rspc3v

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

Ref Expression
Hypotheses rspc3v.1 ⊢ x = A → φ ↔ χ
rspc3v.2 ⊢ y = B → χ ↔ θ
rspc3v.3 ⊢ z = C → θ ↔ ψ
Assertion rspc3v ⊢ A ∈ R ∧ B ∈ S ∧ C ∈ T → ∀ x ∈ R ∀ y ∈ S ∀ z ∈ T φ → ψ

Proof

Step Hyp Ref Expression
1 rspc3v.1 ⊢ x = A → φ ↔ χ
2 rspc3v.2 ⊢ y = B → χ ↔ θ
3 rspc3v.3 ⊢ z = C → θ ↔ ψ
4 1 ralbidv ⊢ x = A → ∀ z ∈ T φ ↔ ∀ z ∈ T χ
5 2 ralbidv ⊢ y = B → ∀ z ∈ T χ ↔ ∀ z ∈ T θ
6 4 5 rspc2v ⊢ A ∈ R ∧ B ∈ S → ∀ x ∈ R ∀ y ∈ S ∀ z ∈ T φ → ∀ z ∈ T θ
7 3 rspcv ⊢ C ∈ T → ∀ z ∈ T θ → ψ
8 6 7 sylan9 ⊢ A ∈ R ∧ B ∈ S ∧ C ∈ T → ∀ x ∈ R ∀ y ∈ S ∀ z ∈ T φ → ψ
9 8 3impa ⊢ A ∈ R ∧ B ∈ S ∧ C ∈ T → ∀ x ∈ R ∀ y ∈ S ∀ z ∈ T φ → ψ