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

Theorem ralrimivvva 2889
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 1218 . . . 4  |-  ( ( ( ( ph  /\  x  e.  A )  /\  y  e.  B
)  /\  z  e.  C )  ->  ps )
32ralrimiva 2881 . . 3  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  A. z  e.  C  ps )
43ralrimiva 2881 . 2  |-  ( (
ph  /\  x  e.  A )  ->  A. y  e.  B  A. z  e.  C  ps )
54ralrimiva 2881 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  A. z  e.  C  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973    e. wcel 1767   A.wral 2817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-ral 2822
This theorem is referenced by:  ispod  4813  swopolem  4814  isopolem  6239  caovassg  6467  caovcang  6470  caovordig  6474  caovordg  6476  caovdig  6483  caovdirg  6486  caofass  6568  caoftrn  6569  2oppccomf  14993  oppccomfpropd  14995  issubc3  15088  fthmon  15166  fuccocl  15203  fucidcl  15204  invfuc  15213  resssetc  15289  resscatc  15302  curf2cl  15370  yonedalem4c  15416  yonedalem3  15419  latdisdlem  15688  isringd  17082  prdsringd  17110  islmodd  17366  islmhm2  17532  isassad  17819  isphld  18535  ocvlss  18549  mdetuni0  18969  mdetmul  18971  psmettri2  20658  isngp4  20976  legso  23827  tglowdim2ln  23860  f1otrgitv  23964  f1otrg  23965  f1otrge  23966  xmstrkgc  23980  eengtrkg  24079  eengtrkge  24080  isgrp2d  25028  isgrpda  25090  isrngod  25172  rngomndo  25214  submomnd  27492  islfld  34152  lfladdcl  34161  lflnegcl  34165  lshpkrcl  34206  lclkr  36623  lclkrs  36629  lcfr  36675
  Copyright terms: Public domain W3C validator