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φ→ψ