This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem r19.40

Description: Restricted quantifier version of Theorem 19.40 of Margaris p. 90. (Contributed by NM, 2-Apr-2004)

Ref Expression
Assertion r19.40 ⊢ ∃ x ∈ A φ ∧ ψ → ∃ x ∈ A φ ∧ ∃ x ∈ A ψ

Proof

Step Hyp Ref Expression
1 simpl ⊢ φ ∧ ψ → φ
2 1 reximi ⊢ ∃ x ∈ A φ ∧ ψ → ∃ x ∈ A φ
3 simpr ⊢ φ ∧ ψ → ψ
4 3 reximi ⊢ ∃ x ∈ A φ ∧ ψ → ∃ x ∈ A ψ
5 2 4 jca ⊢ ∃ x ∈ A φ ∧ ψ → ∃ x ∈ A φ ∧ ∃ x ∈ A ψ