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

Theorem ralrimivvva 2637
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 2627 . . 3  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  A. z  e.  C  ps )
54ralrimiva 2627 . 2  |-  ( (
ph  /\  x  e.  A )  ->  A. y  e.  B  A. z  e.  C  ps )
65ralrimiva 2627 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 1688   A.wral 2544
This theorem is referenced by:  ispod  4321  swopolem  4322  isopolem  5803  caovassg  5979  caovcang  5982  caovordig  5986  caovordg  5988  caovdig  5995  caovdirg  5998  caofass  6072  caoftrn  6073  2oppccomf  13622  oppccomfpropd  13624  issubc3  13717  fthmon  13795  fuccocl  13832  fucidcl  13833  invfuc  13842  resssetc  13918  resscatc  13931  curf2cl  13999  yonedalem4c  14045  yonedalem3  14048  latdisdlem  14286  ismndd  14390  isrngd  15369  prdsrngd  15389  islmodd  15627  islmhm2  15789  isassad  16057  isphld  16552  ocvlss  16566  isngp4  18127  isgrp2d  20894  isgrpda  20956  isrngod  21038  rngomndo  21080  tcnvec  25089  dualcat2  25183  islfld  28519  lfladdcl  28528  lflnegcl  28532  lshpkrcl  28573  lclkr  30990  lclkrs  30996  lcfr  31042
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-11 1719
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 941  df-nf 1537  df-ral 2549
  Copyright terms: Public domain W3C validator