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

Theorem 2exbii 1586
 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 1585 . 2 (∃𝑦𝜑 ↔ ∃𝑦𝜓)
32exbii 1585 1 (∃𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝜓)
 Colors of variables: wff set class Syntax hints:   ↔ wb 104  ∃wex 1472 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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-ial 1514 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  3exbii  1587  19.42vvvv  1893  3exdistr  1895  cbvex4v  1910  ee4anv  1914  ee8anv  1915  sbel2x  1978  2eu4  2099  rexcomf  2619  reean  2625  ceqsex3v  2754  ceqsex4v  2755  ceqsex8v  2757  copsexg  4204  opelopabsbALT  4219  opabm  4240  uniuni  4410  rabxp  4622  elxp3  4639  elvv  4647  elvvv  4648  rexiunxp  4727  elcnv2  4763  cnvuni  4771  coass  5103  fununi  5237  dfmpt3  5291  dfoprab2  5865  dmoprab  5899  rnoprab  5901  mpomptx  5909  resoprab  5914  ovi3  5954  ov6g  5955  oprabex3  6074  xpassen  6772  enq0enq  7345  enq0sym  7346  enq0tr  7348  ltresr  7753  axaddf  7782  axmulf  7783
 Copyright terms: Public domain W3C validator