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

Metamath Proof Explorer

Theorem rspc6v

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

Ref Expression
Hypotheses rspc6v.1 ⊢ x = A → φ ↔ χ
rspc6v.2 ⊢ y = B → χ ↔ θ
rspc6v.3 ⊢ z = C → θ ↔ τ
rspc6v.4 ⊢ w = D → τ ↔ η
rspc6v.5 ⊢ p = E → η ↔ ζ
rspc6v.6 ⊢ q = F → ζ ↔ ψ
Assertion rspc6v ⊢ A ∈ R ∧ B ∈ S ∧ C ∈ T ∧ D ∈ U ∧ E ∈ V ∧ F ∈ W → ∀ x ∈ R ∀ y ∈ S ∀ z ∈ T ∀ w ∈ U ∀ p ∈ V ∀ q ∈ W φ → ψ

Proof

Step Hyp Ref Expression
1 rspc6v.1 ⊢ x = A → φ ↔ χ
2 rspc6v.2 ⊢ y = B → χ ↔ θ
3 rspc6v.3 ⊢ z = C → θ ↔ τ
4 rspc6v.4 ⊢ w = D → τ ↔ η
5 rspc6v.5 ⊢ p = E → η ↔ ζ
6 rspc6v.6 ⊢ q = F → ζ ↔ ψ
7 1 2ralbidv ⊢ x = A → ∀ p ∈ V ∀ q ∈ W φ ↔ ∀ p ∈ V ∀ q ∈ W χ
8 2 2ralbidv ⊢ y = B → ∀ p ∈ V ∀ q ∈ W χ ↔ ∀ p ∈ V ∀ q ∈ W θ
9 3 2ralbidv ⊢ z = C → ∀ p ∈ V ∀ q ∈ W θ ↔ ∀ p ∈ V ∀ q ∈ W τ
10 4 2ralbidv ⊢ w = D → ∀ p ∈ V ∀ q ∈ W τ ↔ ∀ p ∈ V ∀ q ∈ W η
11 7 8 9 10 rspc4v ⊢ A ∈ R ∧ B ∈ S ∧ C ∈ T ∧ D ∈ U → ∀ x ∈ R ∀ y ∈ S ∀ z ∈ T ∀ w ∈ U ∀ p ∈ V ∀ q ∈ W φ → ∀ p ∈ V ∀ q ∈ W η
12 5 6 rspc2v ⊢ E ∈ V ∧ F ∈ W → ∀ p ∈ V ∀ q ∈ W η → ψ
13 11 12 syl9 ⊢ A ∈ R ∧ B ∈ S ∧ C ∈ T ∧ D ∈ U → E ∈ V ∧ F ∈ W → ∀ x ∈ R ∀ y ∈ S ∀ z ∈ T ∀ w ∈ U ∀ p ∈ V ∀ q ∈ W φ → ψ
14 13 3impia ⊢ A ∈ R ∧ B ∈ S ∧ C ∈ T ∧ D ∈ U ∧ E ∈ V ∧ F ∈ W → ∀ x ∈ R ∀ y ∈ S ∀ z ∈ T ∀ w ∈ U ∀ p ∈ V ∀ q ∈ W φ → ψ