Metamath Proof Explorer

Theorem 2r19.29

Description: Theorem r19.29 with two quantifiers. (Contributed by Rodolfo Medina, 25-Sep-2010)

Ref Expression
Assertion 2r19.29 ⊢ ∀ x ∈ A ∀ y ∈ B φ ∧ ∃ x ∈ A ∃ y ∈ B ψ → ∃ x ∈ A ∃ y ∈ B φ ∧ ψ

Proof

Step Hyp Ref Expression
1 r19.29 ⊢ ∀ x ∈ A ∀ y ∈ B φ ∧ ∃ x ∈ A ∃ y ∈ B ψ → ∃ x ∈ A ∀ y ∈ B φ ∧ ∃ y ∈ B ψ
2 r19.29 ⊢ ∀ y ∈ B φ ∧ ∃ y ∈ B ψ → ∃ y ∈ B φ ∧ ψ
3 2 reximi ⊢ ∃ x ∈ A ∀ y ∈ B φ ∧ ∃ y ∈ B ψ → ∃ x ∈ A ∃ y ∈ B φ ∧ ψ
4 1 3 syl ⊢ ∀ x ∈ A ∀ y ∈ B φ ∧ ∃ x ∈ A ∃ y ∈ B ψ → ∃ x ∈ A ∃ y ∈ B φ ∧ ψ