Theorem ralrimivvva

Description: Inference from Theorem 19.21 of Margaris p. 90. (Restricted quantifier version with triple quantification.) (Contributed by Mario Carneiro, 9-Jul-2014)

	Ref	Expression
Hypothesis	ralrimivvva.1	|- ( ( ph /\ ( x e. A /\ y e. B /\ z e. C ) ) -> ps )
Assertion	ralrimivvva	|- ( ph -> A. x e. A A. y e. B A. z e. C ps )

Proof

Step	Hyp	Ref	Expression
1		ralrimivvva.1	|- ( ( ph /\ ( x e. A /\ y e. B /\ z e. C ) ) -> ps )
2	1	3anassrs	|- ( ( ( ( ph /\ x e. A ) /\ y e. B ) /\ z e. C ) -> ps )
3	2	ralrimiva	|- ( ( ( ph /\ x e. A ) /\ y e. B ) -> A. z e. C ps )
4	3	ralrimiva	|- ( ( ph /\ x e. A ) -> A. y e. B A. z e. C ps )
5	4	ralrimiva	|- ( ph -> A. x e. A A. y e. B A. z e. C ps )