Metamath Proof Explorer

Theorem ralimdv2

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005)

Ref Expression
Hypothesis ralimdv2.1 ⊢ φ → x ∈ A → ψ → x ∈ B → χ
Assertion ralimdv2 ⊢ φ → ∀ x ∈ A ψ → ∀ x ∈ B χ

Proof

Step Hyp Ref Expression
1 ralimdv2.1 ⊢ φ → x ∈ A → ψ → x ∈ B → χ
2 1 alimdv ⊢ φ → ∀ x x ∈ A → ψ → ∀ x x ∈ B → χ
3 df-ral ⊢ ∀ x ∈ A ψ ↔ ∀ x x ∈ A → ψ
4 df-ral ⊢ ∀ x ∈ B χ ↔ ∀ x x ∈ B → χ
5 2 3 4 3imtr4g ⊢ φ → ∀ x ∈ A ψ → ∀ x ∈ B χ