Metamath Proof Explorer

Theorem ralimd4v

Description: Deduction quadrupally quantifying both antecedent and consequent. (Contributed by Scott Fenton, 2-Mar-2025) Reduce DV conditions. (Revised by Eric Schmidt, 18-Nov-2025)

Ref Expression
Hypothesis ralimd4v.1 ⊢ φ → ψ → χ
Assertion ralimd4v ⊢ φ → ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ∀ w ∈ D ψ → ∀ x ∈ A ∀ y ∈ B ∀ z ∈ C ∀ w ∈ D χ

Proof

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