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 χ