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  4449  swopolem  4450  ordwe  4723  wessep  4725  isopolem  6028  caovassg  6248  caovcang  6251  caovordig  6255  caovordg  6257  caovdig  6264  caovdirg  6267  caoftrn  6335  netap  7620  2omotaplemap  7623  isrngd  14252  isringd  14346  aprap  14598  islmodd  14629  rnglidlmsgrp  14834  rnglidlrng  14835  isassad  15011