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

Theorem ralrimivvva 2649
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 . . . . . 6  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B  /\  z  e.  C ) )  ->  ps )
213exp2 1169 . . . . 5  |-  ( ph  ->  ( x  e.  A  ->  ( y  e.  B  ->  ( z  e.  C  ->  ps ) ) ) )
32imp41 576 . . . 4  |-  ( ( ( ( ph  /\  x  e.  A )  /\  y  e.  B
)  /\  z  e.  C )  ->  ps )
43ralrimiva 2639 . . 3  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  A. z  e.  C  ps )
54ralrimiva 2639 . 2  |-  ( (
ph  /\  x  e.  A )  ->  A. y  e.  B  A. z  e.  C  ps )
65ralrimiva 2639 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 358    /\ w3a 934    e. wcel 1696   A.wral 2556
This theorem is referenced by:  ispod  4338  swopolem  4339  isopolem  5858  caovassg  6034  caovcang  6037  caovordig  6041  caovordg  6043  caovdig  6050  caovdirg  6053  caofass  6127  caoftrn  6128  2oppccomf  13644  oppccomfpropd  13646  issubc3  13739  fthmon  13817  fuccocl  13854  fucidcl  13855  invfuc  13864  resssetc  13940  resscatc  13953  curf2cl  14021  yonedalem4c  14067  yonedalem3  14070  latdisdlem  14308  ismndd  14412  isrngd  15391  prdsrngd  15411  islmodd  15649  islmhm2  15811  isassad  16079  isphld  16574  ocvlss  16588  isngp4  18149  isgrp2d  20918  isgrpda  20980  isrngod  21062  rngomndo  21104  tcnvec  25793  dualcat2  25887  islfld  29874  lfladdcl  29883  lflnegcl  29887  lshpkrcl  29928  lclkr  32345  lclkrs  32351  lcfr  32397
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-nf 1535  df-ral 2561
  Copyright terms: Public domain W3C validator