Theorem ee4anv 1851

Description: Rearrange existential quantifiers. (Contributed by NM, 31-Jul-1995.)

Assertion

Ref	Expression
ee4anv	|- ( E. x E. y E. z E. w ( ph /\ ps ) <-> ( E. x E. y ph /\ E. z E. w ps ) )

Distinct variable groups:   ph, z   ph, w   ps, x   ps, y   y, z   x, w

Allowed substitution hints:   ph( x, y)   ps( z, w)

Proof of Theorem ee4anv

Step	Hyp	Ref	Expression
1		excom 1595	. . 3 |- ( E. y E. z E. w ( ph /\ ps ) <-> E. z E. y E. w ( ph /\ ps ) )
2	1	exbii 1537	. 2 |- ( E. x E. y E. z E. w ( ph /\ ps ) <-> E. x E. z E. y E. w ( ph /\ ps ) )
3		eeanv 1849	. . 3 |- ( E. y E. w ( ph /\ ps ) <-> ( E. y ph /\ E. w ps ) )
4	3	2exbii 1538	. 2 |- ( E. x E. z E. y E. w ( ph /\ ps ) <-> E. x E. z ( E. y ph /\ E. w ps ) )
5		eeanv 1849	. 2 |- ( E. x E. z ( E. y ph /\ E. w ps ) <-> ( E. x E. y ph /\ E. z E. w ps ) )
6	2, 4, 5	3bitri 204	1 |- ( E. x E. y E. z E. w ( ph /\ ps ) <-> ( E. x E. y ph /\ E. z E. w ps ) )

Syntax hints:   /\ wa 102   <-> 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-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468

This theorem depends on definitions:  df-bi 115  df-nf 1391

This theorem is referenced by:  ee8anv  1852  cgsex4g  2637  th3qlem1  6274  dmaddpq  6631  dmmulpq  6632  ltdcnq  6649  enq0ref  6685  nqpnq0nq  6705  nqnq0a  6706  nqnq0m  6707  genpdisj  6775  axaddcl  7094  axmulcl  7096