ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2exbii GIF version

Theorem 2exbii 1570
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
StepHypRef Expression
1 exbii.1 . . 3 (𝜑𝜓)
21exbii 1569 . 2 (∃𝑦𝜑 ↔ ∃𝑦𝜓)
32exbii 1569 1 (∃𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wb 104  wex 1453
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-ial 1499
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  3exbii  1571  19.42vvvv  1867  3exdistr  1869  cbvex4v  1882  ee4anv  1886  ee8anv  1887  sbel2x  1951  2eu4  2070  rexcomf  2570  reean  2576  ceqsex3v  2702  ceqsex4v  2703  ceqsex8v  2705  copsexg  4136  opelopabsbALT  4151  opabm  4172  uniuni  4342  rabxp  4546  elxp3  4563  elvv  4571  elvvv  4572  rexiunxp  4651  elcnv2  4687  cnvuni  4695  coass  5027  fununi  5161  dfmpt3  5215  dfoprab2  5786  dmoprab  5820  rnoprab  5822  mpomptx  5830  resoprab  5835  ovi3  5875  ov6g  5876  oprabex3  5995  xpassen  6692  enq0enq  7207  enq0sym  7208  enq0tr  7210  ltresr  7615  axaddf  7644  axmulf  7645
  Copyright terms: Public domain W3C validator