Theorem 2ralor

Description: Distribute restricted universal quantification over "or". (Contributed by Jeff Madsen, 19-Jun-2010) (Proof shortened by Wolf Lammen, 20-Nov-2024)

	Ref	Expression
Assertion	2ralor	|- ( A. x e. A A. y e. B ( ph \/ ps ) <-> ( A. x e. A ph \/ A. y e. B ps ) )

Proof

Step	Hyp	Ref	Expression
1		r19.32v	|- ( A. y e. B ( ph \/ ps ) <-> ( ph \/ A. y e. B ps ) )
2		orcom	|- ( ( ph \/ A. y e. B ps ) <-> ( A. y e. B ps \/ ph ) )
3	1 2	bitri	|- ( A. y e. B ( ph \/ ps ) <-> ( A. y e. B ps \/ ph ) )
4	3	ralbii	|- ( A. x e. A A. y e. B ( ph \/ ps ) <-> A. x e. A ( A. y e. B ps \/ ph ) )
5		r19.32v	|- ( A. x e. A ( A. y e. B ps \/ ph ) <-> ( A. y e. B ps \/ A. x e. A ph ) )
6		orcom	|- ( ( A. y e. B ps \/ A. x e. A ph ) <-> ( A. x e. A ph \/ A. y e. B ps ) )
7	4 5 6	3bitri	|- ( A. x e. A A. y e. B ( ph \/ ps ) <-> ( A. x e. A ph \/ A. y e. B ps ) )