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 
|- F/ y ph
19.9d2rf.1 
|- ( ph -> F/ x ps )
19.9d2rf.2 
|- ( ph -> F/ y ps )
19.9d2rf.3 
|- ( ph -> E. x e. A E. y e. B ps )
Assertion 19.9d2rf 
|- ( ph -> ps )

Proof

Step Hyp Ref Expression
1 19.9d2rf.0 
 |-  F/ y ph
2 19.9d2rf.1 
 |-  ( ph -> F/ x ps )
3 19.9d2rf.2 
 |-  ( ph -> F/ y ps )
4 19.9d2rf.3 
 |-  ( ph -> E. x e. A E. y e. B ps )
5 rexex 
 |-  ( E. x e. A E. y e. B ps -> E. x E. y e. B ps )
6 rexex 
 |-  ( E. y e. B ps -> E. y ps )
7 6 eximi 
 |-  ( E. x E. y e. B ps -> E. x E. y ps )
8 4 5 7 3syl 
 |-  ( ph -> E. x E. y ps )
9 1 2 nfexd 
 |-  ( ph -> F/ x E. y ps )
10 9 19.9d 
 |-  ( ph -> ( E. x E. y ps -> E. y ps ) )
11 8 10 mpd 
 |-  ( ph -> E. y ps )
12 3 19.9d 
 |-  ( ph -> ( E. y ps -> ps ) )
13 11 12 mpd 
 |-  ( ph -> ps )