Theorem ralrimivvva 2972

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 1290	. . . 4 |- ( ( ( ( ph /\ x e. A ) /\ y e. B ) /\ z e. C ) -> ps )
3	2	ralrimiva 2966	. . 3 |- ( ( ( ph /\ x e. A ) /\ y e. B ) -> A. z e. C ps )
4	3	ralrimiva 2966	. 2 |- ( ( ph /\ x e. A ) -> A. y e. B A. z e. C ps )
5	4	ralrimiva 2966	1 |- ( ph -> A. x e. A A. y e. B A. z e. C ps )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037   e. wcel 1990   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039  df-ral 2917

This theorem is referenced by:  ispod  5043  swopolem  5044  isopolem  6595  caovassg  6832  caovcang  6835  caovordig  6839  caovordg  6841  caovdig  6848  caovdirg  6851  caofass  6931  caoftrn  6932  2oppccomf  16385  oppccomfpropd  16387  issubc3  16509  fthmon  16587  fuccocl  16624  fucidcl  16625  invfuc  16634  resssetc  16742  resscatc  16755  curf2cl  16871  yonedalem4c  16917  yonedalem3  16920  latdisdlem  17189  isringd  18585  prdsringd  18612  islmodd  18869  islmhm2  19038  isassad  19323  isphld  19999  ocvlss  20016  mdetuni0  20427  mdetmul  20429  isngp4  22416  tglowdim2ln  25546  f1otrgitv  25750  f1otrg  25751  f1otrge  25752  xmstrkgc  25766  eengtrkg  25865  eengtrkge  25866  submomnd  29710  conway  31910  isrngod  33697  rngomndo  33734  isgrpda  33754  islfld  34349  lfladdcl  34358  lflnegcl  34362  lshpkrcl  34403  lclkr  36822  lclkrs  36828  lcfr  36874  copissgrp  41808  lidlmsgrp  41926  lidlrng  41927  cznrng  41955