Theorem 2rexbii 2966

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 2965	. 2 |- ( E. y e. B ph <-> E. y e. B ps )
3	2	rexbii 2965	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 2815

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

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-rex 2820

This theorem is referenced by:  3reeanv  3030  addcompr  9399  mulcompr  9401  4fvwrd4  11790  pythagtriplem2  14200  pythagtrip  14217  efgrelexlemb  16574  ordthaus  19679  regr1lem2  20004  fmucndlem  20557  axpasch  23948  axeuclid  23970  axcontlem4  23974  frgrawopreglem5  24753  xrofsup  27278  ntrivcvgmul  28641  prodmo  28673  poseq  28938  altopelaltxp  29231  brsegle  29363  mzpcompact2lem  30316  sbc4rex  30354  7rexfrabdioph  30365  expdiophlem1  30595  ralnex2  31045  fourierdlem42  31477  ldepslinc  32209