Metamath Proof Explorer

Theorem ralimd6v

Description: Deduction sextupally quantifying both antecedent and consequent. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Hypothesis ralim6dv.1 ⊢ φ → ψ → χ
Assertion ralimd6v ⊢ φ → ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ∀ w ∈ D ∀ p ∈ E ∀ q ∈ F ψ → ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ∀ w ∈ D ∀ p ∈ E ∀ q ∈ F χ

Proof

Step Hyp Ref Expression
1 ralim6dv.1 ⊢ φ → ψ → χ
2 1 ralimdvv ⊢ φ → ∀ p ∈ E ∀ q ∈ F ψ → ∀ p ∈ E ∀ q ∈ F χ
3 2 ralimd4v ⊢ φ → ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ∀ w ∈ D ∀ p ∈ E ∀ q ∈ F ψ → ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ∀ w ∈ D ∀ p ∈ E ∀ q ∈ F χ