Theorem rexcom4a

Description: Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011)

	Ref	Expression
Assertion	rexcom4a	|- ( E. x E. y e. A ( ph /\ ps ) <-> E. y e. A ( ph /\ E. x ps ) )

Proof

Step	Hyp	Ref	Expression
1		rexcom4	|- ( E. y e. A E. x ( ph /\ ps ) <-> E. x E. y e. A ( ph /\ ps ) )
2		19.42v	|- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )
3	2	rexbii	|- ( E. y e. A E. x ( ph /\ ps ) <-> E. y e. A ( ph /\ E. x ps ) )
4	1 3	bitr3i	|- ( E. x E. y e. A ( ph /\ ps ) <-> E. y e. A ( ph /\ E. x ps ) )