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

Theorem ralrimivvva 2636
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 2626 . . 3  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  A. z  e.  C  ps )
54ralrimiva 2626 . 2  |-  ( (
ph  /\  x  e.  A )  ->  A. y  e.  B  A. z  e.  C  ps )
65ralrimiva 2626 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 1684   A.wral 2543
This theorem is referenced by:  ispod  4322  swopolem  4323  isopolem  5842  caovassg  6018  caovcang  6021  caovordig  6025  caovordg  6027  caovdig  6034  caovdirg  6037  caofass  6111  caoftrn  6112  2oppccomf  13628  oppccomfpropd  13630  issubc3  13723  fthmon  13801  fuccocl  13838  fucidcl  13839  invfuc  13848  resssetc  13924  resscatc  13937  curf2cl  14005  yonedalem4c  14051  yonedalem3  14054  latdisdlem  14292  ismndd  14396  isrngd  15375  prdsrngd  15395  islmodd  15633  islmhm2  15795  isassad  16063  isphld  16558  ocvlss  16572  isngp4  18133  isgrp2d  20902  isgrpda  20964  isrngod  21046  rngomndo  21088  tcnvec  25690  dualcat2  25784  islfld  29252  lfladdcl  29261  lflnegcl  29265  lshpkrcl  29306  lclkr  31723  lclkrs  31729  lcfr  31775
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator