Theorem eeanv 1707

Description: Rearrange existential quantifiers.

Assertion

Ref	Expression
eeanv	|- (E.xE.y(ph /\ ps) <-> (E.xph /\ E.yps))

Distinct variable groups:   ph,y   ps,x

Proof of Theorem eeanv

Step	Hyp	Ref	Expression
1		ax-17 1317	. 2 |- (ph -> A.yph)
2		ax-17 1317	. 2 |- (ps -> A.xps)
3	1, 2	eean 1706	1 |- (E.xE.y(ph /\ ps) <-> (E.xph /\ E.yps))

Syntax hints:   <-> wb 163   /\ wa 240  E.wex 1326

This theorem is referenced by:  eeeanv 1708  eeeanvOLD 1709  ee4anv 1710  2eu4 1856  cgsex2g 2322  cgsex4g 2323  vtocl2 2340  vtocl2OLD 2341  cla42egv 2366  csbie2t 2578  dtru 3498  copsex2g 3539  xpnz 4335  fununi 4481  dfoprab5sf 5058  tfrlem7 5125  ener 5469  domtr 5474  unen 5493  sbthlem10 5519  abfii4 5654  aceq5lem4 5900  zorn2lem6 5955  genpn0 6258  genpnnp 6260  mulgt0sr 6366  uzindOLD 7420  creur 7992  creui 7993  replim 8011  subbas 8914  wfrlem4 13960  wfrlem11 13967  axfelem11 14041  elfiun 15369  filssufillem 15570  pcohtpy 16083  riscer 16142  pm11.07 16321

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327

Copyright terms: Public domain