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

Theorem ralrimivvva 2611
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 1174 . . . . 5  |-  ( ph  ->  ( x  e.  A  ->  ( y  e.  B  ->  ( z  e.  C  ->  ps ) ) ) )
32imp41 579 . . . 4  |-  ( ( ( ( ph  /\  x  e.  A )  /\  y  e.  B
)  /\  z  e.  C )  ->  ps )
43ralrimiva 2601 . . 3  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  A. z  e.  C  ps )
54ralrimiva 2601 . 2  |-  ( (
ph  /\  x  e.  A )  ->  A. y  e.  B  A. z  e.  C  ps )
65ralrimiva 2601 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  A. z  e.  C  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    /\ w3a 939    e. wcel 1621   A.wral 2518
This theorem is referenced by:  ispod  4294  swopolem  4295  isopolem  5776  caovassg  5952  caovcang  5955  caovordig  5959  caovordg  5961  caovdig  5968  caovdirg  5971  caofass  6045  caoftrn  6046  2oppccomf  13590  oppccomfpropd  13592  issubc3  13685  fthmon  13763  fuccocl  13800  fucidcl  13801  invfuc  13810  resssetc  13886  resscatc  13899  curf2cl  13967  yonedalem4c  14013  yonedalem3  14016  latdisdlem  14254  ismndd  14358  isrngd  15337  prdsrngd  15357  islmodd  15595  islmhm2  15757  isassad  16025  isphld  16520  ocvlss  16534  isngp4  18095  isgrp2d  20862  isgrpda  20924  isrngod  21006  rngomndo  21048  tcnvec  25057  dualcat2  25151  islfld  28419  lfladdcl  28428  lflnegcl  28432  lshpkrcl  28473  lclkr  30890  lclkrs  30896  lcfr  30942
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 941  df-nf 1540  df-ral 2523
  Copyright terms: Public domain W3C validator