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

Theorem ralrimivvva 2598
 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:   ,,,   ,,   ,
Allowed substitution hints:   (,,)   ()   (,)   (,,)

Proof of Theorem ralrimivvva
StepHypRef Expression
1 ralrimivvva.1 . . . . . 6
213exp2 1174 . . . . 5
32imp41 579 . . . 4
43ralrimiva 2588 . . 3
54ralrimiva 2588 . 2
65ralrimiva 2588 1
 Colors of variables: wff set class Syntax hints:   wi 6   wa 360   w3a 939   wcel 1621  wral 2509 This theorem is referenced by:  ispod  4215  swopolem  4216  isopolem  5694  caovassg  5870  caovcang  5873  caovordig  5877  caovordg  5879  caovdig  5886  caovdirg  5889  caofass  5963  caoftrn  5964  2oppccomf  13472  oppccomfpropd  13474  issubc3  13567  fthmon  13645  fuccocl  13682  fucidcl  13683  invfuc  13692  resssetc  13768  resscatc  13781  curf2cl  13849  yonedalem4c  13895  yonedalem3  13898  latdisdlem  14127  ismndd  14231  isrngd  15210  prdsrngd  15230  islmodd  15468  islmhm2  15630  isassad  15895  isphld  16390  ocvlss  16404  isngp4  17965  isgrp2d  20732  isgrpda  20794  isrngod  20876  rngomndo  20918  tcnvec  24856  dualcat2  24950  islfld  27941  lfladdcl  27950  lflnegcl  27954  lshpkrcl  27995  lclkr  30412  lclkrs  30418  lcfr  30464 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692 This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 941  df-nf 1540  df-ral 2513
 Copyright terms: Public domain W3C validator