Theorem 2exbii 1537

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

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

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 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-ial 1467

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3exbii  1538  19.42vvvv  1831  3exdistr  1833  cbvex4v  1846  ee4anv  1850  ee8anv  1851  sbel2x  1915  2eu4  2034  rexcomf  2516  reean  2522  ceqsex3v  2641  ceqsex4v  2642  ceqsex8v  2644  copsexg  3999  opelopabsbALT  4014  opabm  4035  uniuni  4201  rabxp  4398  elxp3  4412  elvv  4420  elvvv  4421  rexiunxp  4496  elcnv2  4531  cnvuni  4539  coass  4859  fununi  4987  dfmpt3  5041  dfoprab2  5572  dmoprab  5605  rnoprab  5607  mpt2mptx  5615  resoprab  5617  ovi3  5657  ov6g  5658  oprabex3  5776  xpassen  6327  enq0enq  6621  enq0sym  6622  enq0tr  6624  ltresr  7007