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

Theorem ralrimivvva 2598
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 2588 . . 3  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  A. z  e.  C  ps )
54ralrimiva 2588 . 2  |-  ( (
ph  /\  x  e.  A )  ->  A. y  e.  B  A. z  e.  C  ps )
65ralrimiva 2588 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 2509
This theorem is referenced by:  ispod  4215  swopolem  4216  isopolem  5694  caovassg  5870  caovcang  5873  caovordig  5877  caovordg  5879  caovdig  5886  caovdirg  5889  caofass  5963  caoftrn  5964  2oppccomf  13472  oppccomfpropd  13474  issubc3  13567  fthmon  13645  fuccocl  13682  fucidcl  13683  invfuc  13692  resssetc  13768  resscatc  13781  curf2cl  13849  yonedalem4c  13895  yonedalem3  13898  latdisdlem  14127  ismndd  14231  isrngd  15210  prdsrngd  15230  islmodd  15468  islmhm2  15630  isassad  15895  isphld  16390  ocvlss  16404  isngp4  17965  isgrp2d  20732  isgrpda  20794  isrngod  20876  rngomndo  20918  tcnvec  24856  dualcat2  24950  islfld  28156  lfladdcl  28165  lflnegcl  28169  lshpkrcl  28210  lclkr  30627  lclkrs  30633  lcfr  30679
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 2513
  Copyright terms: Public domain W3C validator