Theorem 2exbii 1538

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

Hypothesis

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

Syntax hints:   <-> wb 103   E.wex 1422

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-ial 1468

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3exbii  1539  19.42vvvv  1832  3exdistr  1834  cbvex4v  1847  ee4anv  1851  ee8anv  1852  sbel2x  1916  2eu4  2035  rexcomf  2517  reean  2523  ceqsex3v  2642  ceqsex4v  2643  ceqsex8v  2645  copsexg  4007  opelopabsbALT  4022  opabm  4043  uniuni  4209  rabxp  4406  elxp3  4420  elvv  4428  elvvv  4429  rexiunxp  4506  elcnv2  4541  cnvuni  4549  coass  4869  fununi  4998  dfmpt3  5052  dfoprab2  5583  dmoprab  5616  rnoprab  5618  mpt2mptx  5626  resoprab  5628  ovi3  5668  ov6g  5669  oprabex3  5787  xpassen  6374  enq0enq  6683  enq0sym  6684  enq0tr  6686  ltresr  7069