ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2exbii Unicode 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  |-  ( 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 1567 . 2  |-  ( E. y ph  <->  E. y ps )
32exbii 1567 1  |-  ( E. x E. y ph  <->  E. x E. y ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 104   E.wex 1451
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 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  2567  reean  2573  ceqsex3v  2699  ceqsex4v  2700  ceqsex8v  2702  copsexg  4126  opelopabsbALT  4141  opabm  4162  uniuni  4332  rabxp  4536  elxp3  4553  elvv  4561  elvvv  4562  rexiunxp  4641  elcnv2  4677  cnvuni  4685  coass  5015  fununi  5149  dfmpt3  5203  dfoprab2  5772  dmoprab  5806  rnoprab  5808  mpomptx  5816  resoprab  5821  ovi3  5861  ov6g  5862  oprabex3  5981  xpassen  6677  enq0enq  7187  enq0sym  7188  enq0tr  7190  ltresr  7574  axaddf  7603  axmulf  7604
  Copyright terms: Public domain W3C validator