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

Theorem ralrimivvva 2917
 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 1210 . . . 4
32ralrimiva 2831 . . 3
43ralrimiva 2831 . 2
54ralrimiva 2831 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  /\w3a 965  e.wcel 1758  A.wral 2800 This theorem is referenced by:  ispod  4766  swopolem  4767  isopolem  6167  caovassg  6394  caovcang  6397  caovordig  6401  caovordg  6403  caovdig  6410  caovdirg  6413  caofass  6487  caoftrn  6488  2oppccomf  14823  oppccomfpropd  14825  issubc3  14918  fthmon  14996  fuccocl  15033  fucidcl  15034  invfuc  15043  resssetc  15119  resscatc  15132  curf2cl  15200  yonedalem4c  15246  yonedalem3  15249  latdisdlem  15518  ismndd  15603  isrngd  16855  prdsrngd  16880  islmodd  17130  islmhm2  17295  isassad  17570  isphld  18276  ocvlss  18290  mdetuni0  18695  mdetmul  18697  psmettri2  20284  isngp4  20602  legso  23448  tglowdim2ln  23481  f1otrgitv  23585  f1otrg  23586  f1otrge  23587  xmstrkgc  23601  eengtrkg  23700  eengtrkge  23701  isgrp2d  24191  isgrpda  24253  isrngod  24335  rngomndo  24377  submomnd  26634  islfld  33558  lfladdcl  33567  lflnegcl  33571  lshpkrcl  33612  lclkr  36029  lclkrs  36035  lcfr  36081 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671 This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-ral 2805
 Copyright terms: Public domain W3C validator