Theorem r19.29rOLD

Description: Obsolete version of r19.29r as of 29-Jun-2023. (Contributed by NM, 31-Aug-1999) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	r19.29rOLD	|- ( ( E. x e. A ph /\ A. x e. A ps ) -> E. x e. A ( ph /\ ps ) )

Proof

Step	Hyp	Ref	Expression
1		r19.29	|- ( ( A. x e. A ps /\ E. x e. A ph ) -> E. x e. A ( ps /\ ph ) )
2		ancom	|- ( ( E. x e. A ph /\ A. x e. A ps ) <-> ( A. x e. A ps /\ E. x e. A ph ) )
3		ancom	|- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
4	3	rexbii	|- ( E. x e. A ( ph /\ ps ) <-> E. x e. A ( ps /\ ph ) )
5	1 2 4	3imtr4i	|- ( ( E. x e. A ph /\ A. x e. A ps ) -> E. x e. A ( ph /\ ps ) )