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

Theorem eeanv 1804
 Description: Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.)
Assertion
Ref Expression
eeanv (xy(φ ψ) ↔ (xφ yψ))
Distinct variable groups:   φ,y   ψ,x
Allowed substitution hints:   φ(x)   ψ(y)

Proof of Theorem eeanv
StepHypRef Expression
1 nfv 1418 . 2 yφ
2 nfv 1418 . 2 xψ
31, 2eean 1803 1 (xy(φ ψ) ↔ (xφ yψ))
 Colors of variables: wff set class Syntax hints:   ∧ wa 97   ↔ wb 98  ∃wex 1378 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424 This theorem depends on definitions:  df-bi 110  df-nf 1347 This theorem is referenced by:  eeeanv  1805  ee4anv  1806  2eu4  1990  cgsex2g  2584  cgsex4g  2585  vtocl2  2603  spc2egv  2636  spc2gv  2637  dtruarb  3933  copsex2t  3973  copsex2g  3974  opelopabsb  3988  xpmlem  4687  fununi  4910  imain  4924  brabvv  5493  tfrlem7  5874  ener  6195  domtr  6201  unen  6229  ltexprlemdisj  6580  recexprlemdisj  6602
 Copyright terms: Public domain W3C validator