Theorem 2exbii 1494

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

Hypothesis

Ref	Expression
exbii.1	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
2exbii	⊢ (∃x∃yφ ↔ ∃x∃yψ)

Proof of Theorem 2exbii

Step	Hyp	Ref	Expression
1		exbii.1	. . 3 ⊢ (φ ↔ ψ)
2	1	exbii 1493	. 2 ⊢ (∃yφ ↔ ∃yψ)
3	2	exbii 1493	1 ⊢ (∃x∃yφ ↔ ∃x∃yψ)

Syntax hints:   ↔ wb 98  ∃wex 1378

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-ial 1424

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3exbii  1495  19.42vvvv  1787  3exdistr  1789  cbvex4v  1802  ee4anv  1806  ee8anv  1807  sbel2x  1871  2eu4  1990  rexcomf  2466  reean  2472  ceqsex3v  2590  ceqsex4v  2591  ceqsex8v  2593  copsexg  3972  opelopabsbALT  3987  opabm  4008  uniuni  4149  rabxp  4323  elxp3  4337  elvv  4345  elvvv  4346  rexiunxp  4421  elcnv2  4456  cnvuni  4464  coass  4782  fununi  4910  dfmpt3  4964  dfoprab2  5494  dmoprab  5527  rnoprab  5529  mpt2mptx  5537  resoprab  5539  ovi3  5579  ov6g  5580  oprabex3  5698  xpassen  6240  enq0enq  6414  enq0sym  6415  enq0tr  6417  ltresr  6736