Theorem sepnsepolem1

Description: Lemma for sepnsepo . (Contributed by Zhi Wang, 1-Sep-2024)

	Ref	Expression
Assertion	sepnsepolem1	|- ( E. x e. J E. y e. J ( ph /\ ps /\ ch ) <-> E. x e. J ( ph /\ E. y e. J ( ps /\ ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		3anass	|- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
2	1	2rexbii	|- ( E. x e. J E. y e. J ( ph /\ ps /\ ch ) <-> E. x e. J E. y e. J ( ph /\ ( ps /\ ch ) ) )
3		r19.42v	|- ( E. y e. J ( ph /\ ( ps /\ ch ) ) <-> ( ph /\ E. y e. J ( ps /\ ch ) ) )
4	3	rexbii	|- ( E. x e. J E. y e. J ( ph /\ ( ps /\ ch ) ) <-> E. x e. J ( ph /\ E. y e. J ( ps /\ ch ) ) )
5	2 4	bitri	|- ( E. x e. J E. y e. J ( ph /\ ps /\ ch ) <-> E. x e. J ( ph /\ E. y e. J ( ps /\ ch ) ) )