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

Metamath Proof Explorer

Theorem 19.9d2r

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

Ref Expression
Hypotheses 19.9d2r.1 
|- ( ph -> F/ x ps )
19.9d2r.2 
|- ( ph -> F/ y ps )
19.9d2r.3 
|- ( ph -> E. x e. A E. y e. B ps )
Assertion 19.9d2r 
|- ( ph -> ps )

Proof

Step Hyp Ref Expression
1 19.9d2r.1 
 |-  ( ph -> F/ x ps )
2 19.9d2r.2 
 |-  ( ph -> F/ y ps )
3 19.9d2r.3 
 |-  ( ph -> E. x e. A E. y e. B ps )
4 nfv 
 |-  F/ y ph
5 4 1 2 3 19.9d2rf 
 |-  ( ph -> ps )