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

Metamath Proof Explorer

Theorem 19.9d2rf

Description: A deduction version of one direction of 19.9 with two variables. (Contributed by Thierry Arnoux, 20-Mar-2017)

Ref Expression
Hypotheses 19.9d2rf.0 ⊢ Ⅎ y φ
19.9d2rf.1 ⊢ φ → Ⅎ x ψ
19.9d2rf.2 ⊢ φ → Ⅎ y ψ
19.9d2rf.3 ⊢ φ → ∃ x ∈ A ∃ y ∈ B ψ
Assertion 19.9d2rf ⊢ φ → ψ

Proof

Step Hyp Ref Expression
1 19.9d2rf.0 ⊢ Ⅎ y φ
2 19.9d2rf.1 ⊢ φ → Ⅎ x ψ
3 19.9d2rf.2 ⊢ φ → Ⅎ y ψ
4 19.9d2rf.3 ⊢ φ → ∃ x ∈ A ∃ y ∈ B ψ
5 rexex ⊢ ∃ x ∈ A ∃ y ∈ B ψ → ∃ x ∃ y ∈ B ψ
6 rexex ⊢ ∃ y ∈ B ψ → ∃ y ψ
7 6 eximi ⊢ ∃ x ∃ y ∈ B ψ → ∃ x ∃ y ψ
8 4 5 7 3syl ⊢ φ → ∃ x ∃ y ψ
9 1 2 nfexd ⊢ φ → Ⅎ x ∃ y ψ
10 9 19.9d ⊢ φ → ∃ x ∃ y ψ → ∃ y ψ
11 8 10 mpd ⊢ φ → ∃ y ψ
12 3 19.9d ⊢ φ → ∃ y ψ → ψ
13 11 12 mpd ⊢ φ → ψ