Metamath Proof Explorer

Theorem r19.29d2r

Description: Theorem 19.29 of Margaris p. 90 with two restricted quantifiers, deduction version. (Contributed by Thierry Arnoux, 30-Jan-2017)

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

Proof

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