Theorem 4ralbii

Description: Inference adding four restricted universal quantifiers to both sides of an equivalence. (Contributed by Scott Fenton, 28-Feb-2025)

	Ref	Expression
Hypothesis	4ralbii.1	|- ( ph <-> ps )
Assertion	4ralbii	|- ( A. x e. A A. y e. B A. z e. C A. w e. D ph <-> A. x e. A A. y e. B A. z e. C A. w e. D ps )

Proof

Step	Hyp	Ref	Expression
1		4ralbii.1	|- ( ph <-> ps )
2	1	ralbii	|- ( A. w e. D ph <-> A. w e. D ps )
3	2	3ralbii	|- ( A. x e. A A. y e. B A. z e. C A. w e. D ph <-> A. x e. A A. y e. B A. z e. C A. w e. D ps )