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

Theorem ralrimivvva 2876
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 1216 . . . 4  |-  ( ( ( ( ph  /\  x  e.  A )  /\  y  e.  B
)  /\  z  e.  C )  ->  ps )
32ralrimiva 2868 . . 3  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  A. z  e.  C  ps )
43ralrimiva 2868 . 2  |-  ( (
ph  /\  x  e.  A )  ->  A. y  e.  B  A. z  e.  C  ps )
54ralrimiva 2868 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 367    /\ w3a 971    e. wcel 1823   A.wral 2804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973  df-ral 2809
This theorem is referenced by:  ispod  4797  swopolem  4798  isopolem  6216  caovassg  6446  caovcang  6449  caovordig  6453  caovordg  6455  caovdig  6462  caovdirg  6465  caofass  6547  caoftrn  6548  2oppccomf  15213  oppccomfpropd  15215  issubc3  15337  fthmon  15415  fuccocl  15452  fucidcl  15453  invfuc  15462  resssetc  15570  resscatc  15583  curf2cl  15699  yonedalem4c  15745  yonedalem3  15748  latdisdlem  16018  isringd  17428  prdsringd  17456  islmodd  17713  islmhm2  17879  isassad  18167  isphld  18862  ocvlss  18876  mdetuni0  19290  mdetmul  19292  isngp4  21297  tglowdim2ln  24233  f1otrgitv  24375  f1otrg  24376  f1otrge  24377  xmstrkgc  24391  eengtrkg  24490  eengtrkge  24491  isgrp2d  25435  isgrpda  25497  isrngod  25579  rngomndo  25621  submomnd  27934  copissgrp  32868  lidlmsgrp  32986  lidlrng  32987  cznrng  33017  islfld  35184  lfladdcl  35193  lflnegcl  35197  lshpkrcl  35238  lclkr  37657  lclkrs  37663  lcfr  37709
  Copyright terms: Public domain W3C validator