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