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

Metamath Proof Explorer

Theorem rspc4v

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

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

Proof

Step Hyp Ref Expression
1 rspc4v.1 ⊢ x = A → φ ↔ χ
2 rspc4v.2 ⊢ y = B → χ ↔ θ
3 rspc4v.3 ⊢ z = C → θ ↔ τ
4 rspc4v.4 ⊢ w = D → τ ↔ ψ
5 df-3an ⊢ A ∈ R ∧ B ∈ S ∧ C ∈ T ↔ A ∈ R ∧ B ∈ S ∧ C ∈ T
6 1 ralbidv ⊢ x = A → ∀ w ∈ U φ ↔ ∀ w ∈ U χ
7 2 ralbidv ⊢ y = B → ∀ w ∈ U χ ↔ ∀ w ∈ U θ
8 3 ralbidv ⊢ z = C → ∀ w ∈ U θ ↔ ∀ w ∈ U τ
9 6 7 8 rspc3v ⊢ A ∈ R ∧ B ∈ S ∧ C ∈ T → ∀ x ∈ R ∀ y ∈ S ∀ z ∈ T ∀ w ∈ U φ → ∀ w ∈ U τ
10 4 rspcv ⊢ D ∈ U → ∀ w ∈ U τ → ψ
11 9 10 sylan9 ⊢ A ∈ R ∧ B ∈ S ∧ C ∈ T ∧ D ∈ U → ∀ x ∈ R ∀ y ∈ S ∀ z ∈ T ∀ w ∈ U φ → ψ
12 5 11 sylanbr ⊢ A ∈ R ∧ B ∈ S ∧ C ∈ T ∧ D ∈ U → ∀ x ∈ R ∀ y ∈ S ∀ z ∈ T ∀ w ∈ U φ → ψ
13 12 anasss ⊢ A ∈ R ∧ B ∈ S ∧ C ∈ T ∧ D ∈ U → ∀ x ∈ R ∀ y ∈ S ∀ z ∈ T ∀ w ∈ U φ → ψ