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

Metamath Proof Explorer

Theorem rexlimddv

Description: Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016)

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

Proof

Step Hyp Ref Expression
1 rexlimddv.1 ⊢ φ → ∃ x ∈ A ψ
2 rexlimddv.2 ⊢ φ ∧ x ∈ A ∧ ψ → χ
3 2 rexlimdvaa ⊢ φ → ∃ x ∈ A ψ → χ
4 1 3 mpd ⊢ φ → χ