Metamath Proof Explorer

Theorem 6ralbidv

Description: Formula-building rule for restricted universal quantifiers (deduction form.) (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Hypothesis 6ralbidv.1 ⊢φ→ψ↔χ
Assertion 6ralbidv ⊢φ→∀x∈A∀y∈B∀z∈C∀w∈D∀t∈E∀u∈Fψ↔∀x∈A∀y∈B∀z∈C∀w∈D∀t∈E∀u∈Fχ

Proof

Step Hyp Ref Expression
1 6ralbidv.1 ⊢φ→ψ↔χ
2 1 2ralbidv ⊢φ→∀t∈E∀u∈Fψ↔∀t∈E∀u∈Fχ
3 2 4ralbidv ⊢φ→∀x∈A∀y∈B∀z∈C∀w∈D∀t∈E∀u∈Fψ↔∀x∈A∀y∈B∀z∈C∀w∈D∀t∈E∀u∈Fχ