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

Theorem 2exbii 1538
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 1537 . 2  |-  ( E. y ph  <->  E. y ps )
32exbii 1537 1  |-  ( E. x E. y ph  <->  E. x E. y ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 103   E.wex 1422
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 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-ial 1468
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3exbii  1539  19.42vvvv  1832  3exdistr  1834  cbvex4v  1847  ee4anv  1851  ee8anv  1852  sbel2x  1916  2eu4  2035  rexcomf  2517  reean  2523  ceqsex3v  2642  ceqsex4v  2643  ceqsex8v  2645  copsexg  4007  opelopabsbALT  4022  opabm  4043  uniuni  4209  rabxp  4406  elxp3  4420  elvv  4428  elvvv  4429  rexiunxp  4506  elcnv2  4541  cnvuni  4549  coass  4869  fununi  4998  dfmpt3  5052  dfoprab2  5583  dmoprab  5616  rnoprab  5618  mpt2mptx  5626  resoprab  5628  ovi3  5668  ov6g  5669  oprabex3  5787  xpassen  6374  enq0enq  6683  enq0sym  6684  enq0tr  6686  ltresr  7069
  Copyright terms: Public domain W3C validator