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

Theorem eeanv 1882
Description: Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.)
Assertion
Ref Expression
eeanv  |-  ( E. x E. y (
ph  /\  ps )  <->  ( E. x ph  /\  E. y ps ) )
Distinct variable groups:    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem eeanv
StepHypRef Expression
1 nfv 1491 . 2  |-  F/ y
ph
2 nfv 1491 . 2  |-  F/ x ps
31, 2eean 1881 1  |-  ( E. x E. y (
ph  /\  ps )  <->  ( E. x ph  /\  E. y ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104   E.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-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497
This theorem depends on definitions:  df-bi 116  df-nf 1420
This theorem is referenced by:  eeeanv  1883  ee4anv  1884  2eu4  2068  cgsex2g  2694  cgsex4g  2695  vtocl2  2713  spc2egv  2747  spc2gv  2748  dtruarb  4083  copsex2t  4135  copsex2g  4136  opelopabsb  4150  xpmlem  4927  fununi  5159  imain  5173  brabvv  5783  spc2ed  6096  tfrlem7  6180  ener  6639  domtr  6645  unen  6676  mapen  6706  sbthlemi10  6820  ltexprlemdisj  7378  recexprlemdisj  7402  hashfacen  10519  summodc  11092
  Copyright terms: Public domain W3C validator