Theorem 2rexbii 2889

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 2888	. 2 |- ( E. y e. B ph <-> E. y e. B ps )
3	2	rexbii 2888	1 |- ( E. x e. A E. y e. B ph <-> E. x e. A E. y e. B ps )

Syntax hints:   <-> wb 188   E.wrex 2737

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

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1663  df-rex 2742

This theorem is referenced by:  ralnex2  2892  ralnex3  2893  3reeanv  2958  addcompr  9443  mulcompr  9445  4fvwrd4  11906  ntrivcvgmul  13951  prodmo  13983  pythagtriplem2  14760  pythagtrip  14777  isnsgrp  16524  efgrelexlemb  17393  ordthaus  20393  regr1lem2  20748  fmucndlem  21299  dfcgra2  24864  axpasch  24964  axeuclid  24986  axcontlem4  24990  frgrawopreglem5  25769  xrofsup  28346  poseq  30484  altopelaltxp  30736  brsegle  30868  mzpcompact2lem  35587  sbc4rex  35626  7rexfrabdioph  35637  expdiophlem1  35870  fourierdlem42  38006  fourierdlem42OLD  38007  usgr2edg1  39278  ldepslinc  40289