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

Theorem 2exbii 1538
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 1537 . 2 (∃𝑦𝜑 ↔ ∃𝑦𝜓)
32exbii 1537 1 (∃𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wb 103  wex 1422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-ial 1468
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3exbii  1539  19.42vvvv  1833  3exdistr  1835  cbvex4v  1848  ee4anv  1852  ee8anv  1853  sbel2x  1917  2eu4  2036  rexcomf  2522  reean  2528  ceqsex3v  2652  ceqsex4v  2653  ceqsex8v  2655  copsexg  4035  opelopabsbALT  4050  opabm  4071  uniuni  4237  rabxp  4436  elxp3  4450  elvv  4458  elvvv  4459  rexiunxp  4536  elcnv2  4572  cnvuni  4580  coass  4903  fununi  5035  dfmpt3  5089  dfoprab2  5631  dmoprab  5664  rnoprab  5666  mpt2mptx  5674  resoprab  5676  ovi3  5716  ov6g  5717  oprabex3  5835  xpassen  6476  enq0enq  6893  enq0sym  6894  enq0tr  6896  ltresr  7279
  Copyright terms: Public domain W3C validator