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

Theorem ralrimivvva 2879
 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
Assertion
Ref Expression
ralrimivvva
Distinct variable groups:   ,,,   ,,   ,

Proof of Theorem ralrimivvva
StepHypRef Expression
1 ralrimivvva.1 . . . . 5
213anassrs 1218 . . . 4
32ralrimiva 2871 . . 3
43ralrimiva 2871 . 2
54ralrimiva 2871 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  /\w3a 973  e.wcel 1818  A.wral 2807 This theorem is referenced by:  ispod  4813  swopolem  4814  isopolem  6241  caovassg  6473  caovcang  6476  caovordig  6480  caovordg  6482  caovdig  6489  caovdirg  6492  caofass  6574  caoftrn  6575  2oppccomf  15120  oppccomfpropd  15122  issubc3  15218  fthmon  15296  fuccocl  15333  fucidcl  15334  invfuc  15343  resssetc  15419  resscatc  15432  curf2cl  15500  yonedalem4c  15546  yonedalem3  15549  latdisdlem  15819  isringd  17233  prdsringd  17261  islmodd  17518  islmhm2  17684  isassad  17972  isphld  18689  ocvlss  18703  mdetuni0  19123  mdetmul  19125  isngp4  21131  tglowdim2ln  24032  f1otrgitv  24173  f1otrg  24174  f1otrge  24175  xmstrkgc  24189  eengtrkg  24288  eengtrkge  24289  isgrp2d  25237  isgrpda  25299  isrngod  25381  rngomndo  25423  submomnd  27700  copissgrp  32496  lidlmsgrp  32732  lidlrng  32733  cznrng  32763  islfld  34787  lfladdcl  34796  lflnegcl  34800  lshpkrcl  34841  lclkr  37260  lclkrs  37266  lcfr  37312 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704 This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-ral 2812
 Copyright terms: Public domain W3C validator