Theorem 2exbii 1630

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 1629	. 2 ⊢ (∃𝑦𝜑 ↔ ∃𝑦𝜓)
3	2	exbii 1629	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓)

Syntax hints:   ↔ wb 105  ∃wex 1516

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3exbii  1631  19.42vvvv  1938  3exdistr  1940  cbvex4v  1959  ee4anv  1963  ee8anv  1964  sbel2x  2027  2eu4  2148  rexcomf  2669  reean  2676  ceqsex3v  2816  ceqsex4v  2817  ceqsex8v  2819  copsexg  4292  opelopabsbALT  4309  opabm  4331  uniuni  4502  rabxp  4716  elxp3  4733  elvv  4741  elvvv  4742  rexiunxp  4824  elcnv2  4860  cnvuni  4868  coass  5206  fununi  5347  dfmpt3  5404  dfoprab2  5999  dmoprab  6033  rnoprab  6035  mpomptx  6043  resoprab  6048  ovi3  6090  ov6g  6091  oprabex3  6221  xpassen  6932  enq0enq  7551  enq0sym  7552  enq0tr  7554  ltresr  7959  axaddf  7988  axmulf  7989