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

Theorem ralrimivvva 2865
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 1219 . . . 4  |-  ( ( ( ( ph  /\  x  e.  A )  /\  y  e.  B
)  /\  z  e.  C )  ->  ps )
32ralrimiva 2857 . . 3  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  A. z  e.  C  ps )
43ralrimiva 2857 . 2  |-  ( (
ph  /\  x  e.  A )  ->  A. y  e.  B  A. z  e.  C  ps )
54ralrimiva 2857 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 974    e. wcel 1804   A.wral 2793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 976  df-ral 2798
This theorem is referenced by:  ispod  4798  swopolem  4799  isopolem  6226  caovassg  6458  caovcang  6461  caovordig  6465  caovordg  6467  caovdig  6474  caovdirg  6477  caofass  6559  caoftrn  6560  2oppccomf  14997  oppccomfpropd  14999  issubc3  15092  fthmon  15170  fuccocl  15207  fucidcl  15208  invfuc  15217  resssetc  15293  resscatc  15306  curf2cl  15374  yonedalem4c  15420  yonedalem3  15423  latdisdlem  15693  isringd  17107  prdsringd  17135  islmodd  17392  islmhm2  17558  isassad  17846  isphld  18562  ocvlss  18576  mdetuni0  18996  mdetmul  18998  isngp4  21004  tglowdim2ln  23904  f1otrgitv  24045  f1otrg  24046  f1otrge  24047  xmstrkgc  24061  eengtrkg  24160  eengtrkge  24161  isgrp2d  25109  isgrpda  25171  isrngod  25253  rngomndo  25295  submomnd  27573  copissgrp  32333  lidlmsgrp  32442  lidlrng  32443  cznrng  32473  islfld  34527  lfladdcl  34536  lflnegcl  34540  lshpkrcl  34581  lclkr  37000  lclkrs  37006  lcfr  37052
  Copyright terms: Public domain W3C validator