Theorem ralrimivvva 2580

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

Hypothesis

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

Assertion

Ref	Expression
ralrimivvva	|- ( ph -> A. x e. A A. y e. B A. z e. C ps )

Distinct variable groups:   ph, x, y, z   y, A, z   z, B

Allowed substitution hints:   ps( x, y, z)   A( x)   B( x, y)   C( x, y, z)

Proof of Theorem ralrimivvva

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980   e. wcel 2167   A.wral 2475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-3an 982  df-nf 1475  df-ral 2480

This theorem is referenced by:  ispod  4340  swopolem  4341  ordwe  4613  wessep  4615  isopolem  5872  caovassg  6086  caovcang  6089  caovordig  6093  caovordg  6095  caovdig  6102  caovdirg  6105  caoftrn  6172  netap  7337  2omotaplemap  7340  isrngd  13585  isringd  13673  aprap  13918  islmodd  13925  rnglidlmsgrp  14129  rnglidlrng  14130