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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009   e. wcel 2209   A.wral 2528

This proof depends on 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 proof depends on definitions:  df-bi 117  df-3an 1011  df-nf 1514  df-ral 2533

This theorem is used by:  ispod  4451  swopolem  4452  ordwe  4725  wessep  4727  isopolem  6031  caovassg  6251  caovcang  6254  caovordig  6258  caovordg  6260  caovdig  6267  caovdirg  6270  caoftrn  6339  netap  7626  2omotaplemap  7629  isrngd  14359  isringd  14453  aprap  14707  islmodd  14738  rnglidlmsgrp  14943  rnglidlrng  14944  isassad  15120