ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2exbii Unicode 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  |-  ( ph  <->  ps )
Assertion
Ref Expression
2exbii  |-  ( E. x E. y ph  <->  E. x E. y ps )

Proof of Theorem 2exbii
StepHypRef Expression
1 exbii.1 . . 3  |-  ( ph  <->  ps )
21exbii 1585 . 2  |-  ( E. y ph  <->  E. y ps )
32exbii 1585 1  |-  ( E. x E. y ph  <->  E. x E. y ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 104   E.wex 1469
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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-ial 1515
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  3exbii  1587  19.42vvvv  1886  3exdistr  1888  cbvex4v  1903  ee4anv  1907  ee8anv  1908  sbel2x  1974  2eu4  2093  rexcomf  2596  reean  2602  ceqsex3v  2731  ceqsex4v  2732  ceqsex8v  2734  copsexg  4173  opelopabsbALT  4188  opabm  4209  uniuni  4379  rabxp  4583  elxp3  4600  elvv  4608  elvvv  4609  rexiunxp  4688  elcnv2  4724  cnvuni  4732  coass  5064  fununi  5198  dfmpt3  5252  dfoprab2  5825  dmoprab  5859  rnoprab  5861  mpomptx  5869  resoprab  5874  ovi3  5914  ov6g  5915  oprabex3  6034  xpassen  6731  enq0enq  7262  enq0sym  7263  enq0tr  7265  ltresr  7670  axaddf  7699  axmulf  7700
  Copyright terms: Public domain W3C validator