Theorem 2exbii 1586

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

Syntax hints:   ↔ wb 104  ∃wex 1472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3exbii  1587  19.42vvvv  1893  3exdistr  1895  cbvex4v  1910  ee4anv  1914  ee8anv  1915  sbel2x  1978  2eu4  2099  rexcomf  2619  reean  2625  ceqsex3v  2754  ceqsex4v  2755  ceqsex8v  2757  copsexg  4204  opelopabsbALT  4219  opabm  4240  uniuni  4410  rabxp  4622  elxp3  4639  elvv  4647  elvvv  4648  rexiunxp  4727  elcnv2  4763  cnvuni  4771  coass  5103  fununi  5237  dfmpt3  5291  dfoprab2  5865  dmoprab  5899  rnoprab  5901  mpomptx  5909  resoprab  5914  ovi3  5954  ov6g  5955  oprabex3  6074  xpassen  6772  enq0enq  7345  enq0sym  7346  enq0tr  7348  ltresr  7753  axaddf  7782  axmulf  7783