Metamath Proof Explorer

Theorem 19.29r2

Description: Variation of 19.29r with double quantification. (Contributed by NM, 3-Feb-2005)

Ref Expression
Assertion 19.29r2 ⊢ ∃ x ∃ y φ ∧ ∀ x ∀ y ψ → ∃ x ∃ y φ ∧ ψ

Proof

Step Hyp Ref Expression
1 19.29r ⊢ ∃ x ∃ y φ ∧ ∀ x ∀ y ψ → ∃ x ∃ y φ ∧ ∀ y ψ
2 19.29r ⊢ ∃ y φ ∧ ∀ y ψ → ∃ y φ ∧ ψ
3 2 eximi ⊢ ∃ x ∃ y φ ∧ ∀ y ψ → ∃ x ∃ y φ ∧ ψ
4 1 3 syl ⊢ ∃ x ∃ y φ ∧ ∀ x ∀ y ψ → ∃ x ∃ y φ ∧ ψ