Metamath Proof Explorer

Theorem 6ralimi

Description: Inference quantifying both antecedent and consequent six times, with strong hypothesis. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Hypothesis 2ralimi.1 ⊢ φ → ψ
Assertion 6ralimi ⊢ ∀ 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 2ralimi.1 ⊢ φ → ψ
2 1 ralimi ⊢ ∀ u ∈ F φ → ∀ u ∈ F ψ
3 2 5ralimi ⊢ ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ∀ w ∈ D ∀ t ∈ E ∀ u ∈ F φ → ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ∀ w ∈ D ∀ t ∈ E ∀ u ∈ F ψ