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 ⊢ Ⅎ 𝑦 𝜑
19.9d2rf.1 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
19.9d2rf.2 ⊢ ( 𝜑 → Ⅎ 𝑦 𝜓 )
19.9d2rf.3 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 )
Assertion 19.9d2rf ( 𝜑 → 𝜓 )

Proof

Step Hyp Ref Expression
1 19.9d2rf.0 ⊢ Ⅎ 𝑦 𝜑
2 19.9d2rf.1 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
3 19.9d2rf.2 ⊢ ( 𝜑 → Ⅎ 𝑦 𝜓 )
4 19.9d2rf.3 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 )
5 rexex ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 → ∃ 𝑥 ∃ 𝑦 ∈ 𝐵 𝜓 )
6 rexex ⊢ ( ∃ 𝑦 ∈ 𝐵 𝜓 → ∃ 𝑦 𝜓 )
7 6 eximi ⊢ ( ∃ 𝑥 ∃ 𝑦 ∈ 𝐵 𝜓 → ∃ 𝑥 ∃ 𝑦 𝜓 )
8 4 5 7 3syl ⊢ ( 𝜑 → ∃ 𝑥 ∃ 𝑦 𝜓 )
9 1 2 nfexd ⊢ ( 𝜑 → Ⅎ 𝑥 ∃ 𝑦 𝜓 )
10 9 19.9d ⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 𝜓 → ∃ 𝑦 𝜓 ) )
11 8 10 mpd ⊢ ( 𝜑 → ∃ 𝑦 𝜓 )
12 3 19.9d ⊢ ( 𝜑 → ( ∃ 𝑦 𝜓 → 𝜓 ) )
13 11 12 mpd ⊢ ( 𝜑 → 𝜓 )