Theorem 2exbii 1636

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

Hypothesis

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

Assertion

Ref	Expression
2exbii	|- ( E. x E. y ph <-> E. x E. y ps )

Proof of Theorem 2exbii

Step	Hyp	Ref	Expression
1		2exbii.1	. . 3 |- ( ph <-> ps )
2	1	exbii 1635	. 2 |- ( E. y ph <-> E. y ps )
3	2	exbii 1635	1 |- ( E. x E. y ph <-> E. x E. y ps )

Syntax hints:   <-> wb 184   E.wex 1587

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

This theorem depends on definitions:  df-bi 185  df-ex 1588

This theorem is referenced by:  3exbii  1637  3exdistr  1941  eeeanv  1945  ee4anv  1946  cbvex4v  1994  2sb5rf  2168  sbel2x  2178  sbel2xOLD  2179  2exsb  2191  2mo2  2368  2moOLD  2370  2eu4OLD  2378  2eu6OLD  2381  rexcomf  2986  reean  2993  ceqsex3v  3118  ceqsex4v  3119  ceqsex8v  3121  vtocl3  3132  copsexg  4687  copsexgOLD  4688  opelopabsbALT  4709  opabn0  4730  rabxp  4986  elxp3  5000  elvv  5008  elvvv  5009  copsex2gb  5061  elcnv2  5128  cnvuni  5137  xpdifid  5377  coass  5467  fununi  5595  dfmpt3  5644  dfoprab2  6245  dmoprab  6284  rnoprab  6286  mpt2mptx  6294  resoprab  6299  elrnmpt2res  6317  ov3  6340  ov6g  6341  uniuni  6498  oprabex3  6679  oeeu  7155  xpassen  7518  zorn2lem6  8785  ltresr  9422  axaddf  9427  axmulf  9428  hashfun  12321  5oalem7  25242  mpt2mptxf  26173  eulerpartlemgvv  26926  elima4  27757  wfrlem4  27894  brtxp2  28079  brpprod3a  28084  brpprod3b  28085  elfuns  28113  brcart  28130  brimg  28135  brapply  28136  brsuccf  28139  brrestrict  28147  dfrdg4  28148  ellines  28350  itg2addnclem3  28616  pm11.52  29810  2exanali  29811  pm11.6  29816  pm11.7  29820  stoweidlem35  30001  mpt2mptx2  30895  opelopab4  31615  bnj600  32267  bnj916  32281  bnj983  32299  bnj986  32302  bnj996  32303  bnj1021  32312  bj-cbvex4vv  32601  dalem20  33700  dvhopellsm  35125  diblsmopel  35179