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

Theorem ralrimivvva 2807
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 1204 . . . 4  |-  ( ( ( ( ph  /\  x  e.  A )  /\  y  e.  B
)  /\  z  e.  C )  ->  ps )
32ralrimiva 2797 . . 3  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  A. z  e.  C  ps )
43ralrimiva 2797 . 2  |-  ( (
ph  /\  x  e.  A )  ->  A. y  e.  B  A. z  e.  C  ps )
54ralrimiva 2797 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 960    e. wcel 1761   A.wral 2713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 962  df-ex 1592  df-nf 1595  df-ral 2718
This theorem is referenced by:  ispod  4645  swopolem  4646  isopolem  6033  caovassg  6260  caovcang  6263  caovordig  6267  caovordg  6269  caovdig  6276  caovdirg  6279  caofass  6353  caoftrn  6354  2oppccomf  14660  oppccomfpropd  14662  issubc3  14755  fthmon  14833  fuccocl  14870  fucidcl  14871  invfuc  14880  resssetc  14956  resscatc  14969  curf2cl  15037  yonedalem4c  15083  yonedalem3  15086  latdisdlem  15355  ismndd  15440  isrngd  16669  prdsrngd  16694  islmodd  16934  islmhm2  17097  isassad  17372  isphld  17983  ocvlss  17997  mdetuni0  18327  mdetmul  18329  psmettri2  19785  isngp4  20103  f1otrgitv  23035  f1otrg  23036  f1otrge  23037  xmstrkgc  23051  eengtrkg  23150  eengtrkge  23151  isgrp2d  23641  isgrpda  23703  isrngod  23785  rngomndo  23827  submomnd  26090  islfld  32395  lfladdcl  32404  lflnegcl  32408  lshpkrcl  32449  lclkr  34866  lclkrs  34872  lcfr  34918
  Copyright terms: Public domain W3C validator