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

Theorem ralrimivvva 2809
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 . . . . 5  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B  /\  z  e.  C ) )  ->  ps )
213anassrs 1209 . . . 4  |-  ( ( ( ( ph  /\  x  e.  A )  /\  y  e.  B
)  /\  z  e.  C )  ->  ps )
32ralrimiva 2799 . . 3  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  A. z  e.  C  ps )
43ralrimiva 2799 . 2  |-  ( (
ph  /\  x  e.  A )  ->  A. y  e.  B  A. z  e.  C  ps )
54ralrimiva 2799 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  A. z  e.  C  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965    e. wcel 1756   A.wral 2715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-ex 1587  df-nf 1590  df-ral 2720
This theorem is referenced by:  ispod  4649  swopolem  4650  isopolem  6036  caovassg  6261  caovcang  6264  caovordig  6268  caovordg  6270  caovdig  6277  caovdirg  6280  caofass  6354  caoftrn  6355  2oppccomf  14664  oppccomfpropd  14666  issubc3  14759  fthmon  14837  fuccocl  14874  fucidcl  14875  invfuc  14884  resssetc  14960  resscatc  14973  curf2cl  15041  yonedalem4c  15087  yonedalem3  15090  latdisdlem  15359  ismndd  15444  isrngd  16679  prdsrngd  16704  islmodd  16954  islmhm2  17119  isassad  17394  isphld  18083  ocvlss  18097  mdetuni0  18427  mdetmul  18429  psmettri2  19885  isngp4  20203  f1otrgitv  23116  f1otrg  23117  f1otrge  23118  xmstrkgc  23132  eengtrkg  23231  eengtrkge  23232  isgrp2d  23722  isgrpda  23784  isrngod  23866  rngomndo  23908  submomnd  26173  islfld  32707  lfladdcl  32716  lflnegcl  32720  lshpkrcl  32761  lclkr  35178  lclkrs  35184  lcfr  35230
  Copyright terms: Public domain W3C validator