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

Metamath Proof Explorer

Theorem reximddv

Description: Deduction from Theorem 19.22 of Margaris p. 90. (Contributed by Thierry Arnoux, 7-Dec-2016)

Ref Expression
Hypotheses reximddva.1 ⊢ φ ∧ x ∈ A ∧ ψ → χ
reximddva.2 ⊢ φ → ∃ x ∈ A ψ
Assertion reximddv ⊢ φ → ∃ x ∈ A χ

Proof

Step Hyp Ref Expression
1 reximddva.1 ⊢ φ ∧ x ∈ A ∧ ψ → χ
2 reximddva.2 ⊢ φ → ∃ x ∈ A ψ
3 1 expr ⊢ φ ∧ x ∈ A → ψ → χ
4 3 reximdva ⊢ φ → ∃ x ∈ A ψ → ∃ x ∈ A χ
5 2 4 mpd ⊢ φ → ∃ x ∈ A χ