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

Theorem 2exbii 1542
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 1541 . 2 (∃𝑦𝜑 ↔ ∃𝑦𝜓)
32exbii 1541 1 (∃𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wb 103  wex 1426
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 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-ial 1472
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3exbii  1543  19.42vvvv  1838  3exdistr  1840  cbvex4v  1853  ee4anv  1857  ee8anv  1858  sbel2x  1922  2eu4  2041  rexcomf  2529  reean  2535  ceqsex3v  2661  ceqsex4v  2662  ceqsex8v  2664  copsexg  4062  opelopabsbALT  4077  opabm  4098  uniuni  4264  rabxp  4463  elxp3  4480  elvv  4488  elvvv  4489  rexiunxp  4566  elcnv2  4602  cnvuni  4610  coass  4936  fununi  5068  dfmpt3  5122  dfoprab2  5678  dmoprab  5711  rnoprab  5713  mpt2mptx  5721  resoprab  5723  ovi3  5763  ov6g  5764  oprabex3  5882  xpassen  6526  enq0enq  6969  enq0sym  6970  enq0tr  6972  ltresr  7355
  Copyright terms: Public domain W3C validator