Theorem ralrimivvva 2633

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1009   e. wcel 2209   A.wral 2528

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-nf 1514  df-ral 2533

This theorem is referenced by:  ispod  4444  swopolem  4445  ordwe  4718  wessep  4720  isopolem  6018  caovassg  6238  caovcang  6241  caovordig  6245  caovordg  6247  caovdig  6254  caovdirg  6257  caoftrn  6325  netap  7610  2omotaplemap  7613  isrngd  14227  isringd  14319  aprap  14571  islmodd  14602  rnglidlmsgrp  14806  rnglidlrng  14807