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

Step	Hyp	Ref	Expression
1		ralrimivvva.1	. . . . 5
2	1	3anassrs 1218	. . . 4
3	2	ralrimiva 2871	. . 3
4	3	ralrimiva 2871	. 2
5	4	ralrimiva 2871	1

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