Theorem ralrimivvva 2589

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 981   e. wcel 2176   A.wral 2484

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-3an 983  df-nf 1484  df-ral 2489

This theorem is referenced by:  ispod  4352  swopolem  4353  ordwe  4625  wessep  4627  isopolem  5893  caovassg  6107  caovcang  6110  caovordig  6114  caovordg  6116  caovdig  6123  caovdirg  6126  caoftrn  6193  netap  7368  2omotaplemap  7371  isrngd  13748  isringd  13836  aprap  14081  islmodd  14088  rnglidlmsgrp  14292  rnglidlrng  14293