MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralrimivvva Unicode version

Theorem ralrimivvva 2791
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
StepHypRef Expression
1 ralrimivvva.1 . . . . 5  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B  /\  z  e.  C ) )  ->  ps )
213anassrs 1175 . . . 4  |-  ( ( ( ( ph  /\  x  e.  A )  /\  y  e.  B
)  /\  z  e.  C )  ->  ps )
32ralrimiva 2781 . . 3  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  A. z  e.  C  ps )
43ralrimiva 2781 . 2  |-  ( (
ph  /\  x  e.  A )  ->  A. y  e.  B  A. z  e.  C  ps )
54ralrimiva 2781 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  A. z  e.  C  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936    e. wcel 1725   A.wral 2697
This theorem is referenced by:  ispod  4503  swopolem  4504  isopolem  6056  caovassg  6236  caovcang  6239  caovordig  6243  caovordg  6245  caovdig  6252  caovdirg  6255  caofass  6329  caoftrn  6330  2oppccomf  13939  oppccomfpropd  13941  issubc3  14034  fthmon  14112  fuccocl  14149  fucidcl  14150  invfuc  14159  resssetc  14235  resscatc  14248  curf2cl  14316  yonedalem4c  14362  yonedalem3  14365  latdisdlem  14603  ismndd  14707  isrngd  15686  prdsrngd  15706  islmodd  15944  islmhm2  16102  isassad  16370  isphld  16873  ocvlss  16887  psmettri2  18328  isngp4  18646  isgrp2d  21811  isgrpda  21873  isrngod  21955  rngomndo  21997  islfld  29699  lfladdcl  29708  lflnegcl  29712  lshpkrcl  29753  lclkr  32170  lclkrs  32176  lcfr  32222
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-ex 1551  df-nf 1554  df-ral 2702
  Copyright terms: Public domain W3C validator