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

Theorem eeanv 1855
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 1466 . 2  |-  F/ y
ph
2 nfv 1466 . 2  |-  F/ x ps
31, 2eean 1854 1  |-  ( E. x E. y (
ph  /\  ps )  <->  ( E. x ph  /\  E. y ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 102    <-> wb 103   E.wex 1426
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 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472
This theorem depends on definitions:  df-bi 115  df-nf 1395
This theorem is referenced by:  eeeanv  1856  ee4anv  1857  2eu4  2041  cgsex2g  2655  cgsex4g  2656  vtocl2  2674  spc2egv  2708  spc2gv  2709  dtruarb  4017  copsex2t  4063  copsex2g  4064  opelopabsb  4078  xpmlem  4839  fununi  5068  imain  5082  brabvv  5677  spc2ed  5980  tfrlem7  6064  ener  6476  domtr  6482  unen  6513  mapen  6542  sbthlemi10  6654  ltexprlemdisj  7144  recexprlemdisj  7168  hashfacen  10206  isummo  10737
  Copyright terms: Public domain W3C validator