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

Theorem 2exbii 1513
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 1512 . 2 (∃𝑦𝜑 ↔ ∃𝑦𝜓)
32exbii 1512 1 (∃𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wb 102  wex 1397
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-ial 1443
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  3exbii  1514  19.42vvvv  1806  3exdistr  1808  cbvex4v  1821  ee4anv  1825  ee8anv  1826  sbel2x  1890  2eu4  2009  rexcomf  2489  reean  2495  ceqsex3v  2613  ceqsex4v  2614  ceqsex8v  2616  copsexg  4008  opelopabsbALT  4023  opabm  4044  uniuni  4210  rabxp  4407  elxp3  4421  elvv  4429  elvvv  4430  rexiunxp  4505  elcnv2  4540  cnvuni  4548  coass  4866  fununi  4994  dfmpt3  5048  dfoprab2  5579  dmoprab  5612  rnoprab  5614  mpt2mptx  5622  resoprab  5624  ovi3  5664  ov6g  5665  oprabex3  5783  xpassen  6334  enq0enq  6586  enq0sym  6587  enq0tr  6589  ltresr  6972
  Copyright terms: Public domain W3C validator