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

Theorem 2exbii 1568
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 1567 . 2 (∃𝑦𝜑 ↔ ∃𝑦𝜓)
32exbii 1567 1 (∃𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wb 104  wex 1451
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-ial 1497
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  3exbii  1569  19.42vvvv  1865  3exdistr  1867  cbvex4v  1880  ee4anv  1884  ee8anv  1885  sbel2x  1949  2eu4  2068  rexcomf  2568  reean  2574  ceqsex3v  2700  ceqsex4v  2701  ceqsex8v  2703  copsexg  4134  opelopabsbALT  4149  opabm  4170  uniuni  4340  rabxp  4544  elxp3  4561  elvv  4569  elvvv  4570  rexiunxp  4649  elcnv2  4685  cnvuni  4693  coass  5025  fununi  5159  dfmpt3  5213  dfoprab2  5784  dmoprab  5818  rnoprab  5820  mpomptx  5828  resoprab  5833  ovi3  5873  ov6g  5874  oprabex3  5993  xpassen  6690  enq0enq  7203  enq0sym  7204  enq0tr  7206  ltresr  7611  axaddf  7640  axmulf  7641
  Copyright terms: Public domain W3C validator