Theorem ralrimivvva 2573

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980   e. wcel 2160   A.wral 2468

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-3an 982  df-nf 1472  df-ral 2473

This theorem is referenced by:  ispod  4319  swopolem  4320  ordwe  4590  wessep  4592  isopolem  5839  caovassg  6050  caovcang  6053  caovordig  6057  caovordg  6059  caovdig  6066  caovdirg  6069  caoftrn  6126  netap  7272  2omotaplemap  7275  isrngd  13274  isringd  13362  aprap  13569  islmodd  13576  rnglidlmsgrp  13780  rnglidlrng  13781