Theorem 2rexbii 2960

Description: Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)

Hypothesis

Ref	Expression
rexbii.1	|- ( ph <-> ps )

Assertion

Ref	Expression
2rexbii	|- ( E. x e. A E. y e. B ph <-> E. x e. A E. y e. B ps )

Proof of Theorem 2rexbii

Step	Hyp	Ref	Expression
1		rexbii.1	. . 3 |- ( ph <-> ps )
2	1	rexbii 2959	. 2 |- ( E. y e. B ph <-> E. y e. B ps )
3	2	rexbii 2959	1 |- ( E. x e. A E. y e. B ph <-> E. x e. A E. y e. B ps )

Syntax hints:   <-> wb 184   E.wrex 2808

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1614  df-rex 2813

This theorem is referenced by:  3reeanv  3026  addcompr  9416  mulcompr  9418  4fvwrd4  11819  ntrivcvgmul  13723  prodmo  13755  pythagtriplem2  14353  pythagtrip  14370  isnsgrp  16042  efgrelexlemb  16895  ordthaus  20012  regr1lem2  20367  fmucndlem  20920  axpasch  24371  axeuclid  24393  axcontlem4  24397  frgrawopreglem5  25175  xrofsup  27742  poseq  29550  altopelaltxp  29831  brsegle  29963  mzpcompact2lem  30889  sbc4rex  30927  7rexfrabdioph  30938  expdiophlem1  31167  ralnex2  31638  fourierdlem42  32134  ldepslinc  33254