Theorem 2exbii 1714

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 1713	. 2 |- ( E. y ph <-> E. y ps )
3	2	exbii 1713	1 |- ( E. x E. y ph <-> E. x E. y ps )

Syntax hints:   <-> wb 188   E.wex 1660

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

This theorem depends on definitions:  df-bi 189  df-ex 1661

This theorem is referenced by:  3exbii  1715  3exdistr  1829  eeeanv  2045  ee4anv  2046  cbvex4v  2088  2sb5rf  2247  sbel2x  2255  2exsb  2265  2mo2  2347  2moOLD  2349  rexcomf  2989  reean  2996  ceqsex3v  3122  ceqsex4v  3123  ceqsex8v  3125  vtocl3  3136  copsexg  4705  opelopabsbALT  4728  opabn0  4750  rabxp  4889  elxp3  4903  elvv  4911  elvvv  4912  copsex2gb  4963  elcnv2  5030  cnvuni  5039  xpdifid  5283  coass  5372  fununi  5666  dfmpt3  5715  tpres  6131  dfoprab2  6350  dmoprab  6390  rnoprab  6392  mpt2mptx  6400  resoprab  6405  elrnmpt2res  6423  ov3  6446  ov6g  6447  uniuni  6613  oprabex3  6795  wfrlem4  7049  oeeu  7314  xpassen  7674  zorn2lem6  8937  ltresr  9570  axaddf  9575  axmulf  9576  hashfun  12612  5oalem7  27309  mpt2mptxf  28280  eulerpartlemgvv  29215  bnj600  29736  bnj916  29750  bnj983  29768  bnj986  29771  bnj996  29772  bnj1021  29781  elima4  30426  brtxp2  30651  brpprod3a  30656  brpprod3b  30657  elfuns  30685  brcart  30702  brimg  30707  brapply  30708  brsuccf  30711  brrestrict  30719  dfrdg4  30721  ellines  30922  bj-cbvex4vv  31306  itg2addnclem3  31957  dalem20  33225  dvhopellsm  34652  diblsmopel  34706  pm11.52  36642  2exanali  36643  pm11.6  36648  pm11.7  36652  opelopab4  36824  stoweidlem35  37764  mpt2mptx2  39510