Theorem 2exbii 1632

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	⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)

Proof of Theorem 2exbii

Step	Hyp	Ref	Expression
1		exbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	exbii 1631	. 2 ⊢ (∃𝑦𝜑 ↔ ∃𝑦𝜓)
3	2	exbii 1631	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)

Syntax hints:   ↔ wb 105  ∃wex 1518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1473  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-4 1536  ax-ial 1560

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3exbii  1633  19.42vvvv  1940  3exdistr  1942  cbvex4v  1961  ee4anv  1965  ee8anv  1966  sbel2x  2029  2eu4  2151  rexcomf  2673  reean  2680  ceqsex3v  2823  ceqsex4v  2824  ceqsex8v  2826  copsexg  4309  opelopabsbALT  4326  opabm  4348  uniuni  4519  rabxp  4733  elxp3  4750  elvv  4758  elvvv  4759  rexiunxp  4841  elcnv2  4877  cnvuni  4885  coass  5223  fununi  5365  dfmpt3  5422  dfoprab2  6022  dmoprab  6056  rnoprab  6058  mpomptx  6066  resoprab  6071  ovi3  6113  ov6g  6114  oprabex3  6244  xpassen  6957  enq0enq  7586  enq0sym  7587  enq0tr  7589  ltresr  7994  axaddf  8023  axmulf  8024