Theorem 2exbii 1616

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

Syntax hints:   ↔ wb 105  ∃wex 1502

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-ial 1544

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3exbii  1617  19.42vvvv  1923  3exdistr  1925  cbvex4v  1940  ee4anv  1944  ee8anv  1945  sbel2x  2008  2eu4  2129  rexcomf  2649  reean  2656  ceqsex3v  2791  ceqsex4v  2792  ceqsex8v  2794  copsexg  4256  opelopabsbALT  4271  opabm  4292  uniuni  4463  rabxp  4675  elxp3  4692  elvv  4700  elvvv  4701  rexiunxp  4781  elcnv2  4817  cnvuni  4825  coass  5159  fununi  5296  dfmpt3  5350  dfoprab2  5935  dmoprab  5969  rnoprab  5971  mpomptx  5979  resoprab  5984  ovi3  6025  ov6g  6026  oprabex3  6144  xpassen  6844  enq0enq  7444  enq0sym  7445  enq0tr  7447  ltresr  7852  axaddf  7881  axmulf  7882