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

Theorem ralrimivvva 3197
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 . . . . 5 ((𝜑 ∧ (𝑥𝐴𝑦𝐵𝑧𝐶)) → 𝜓)
213anassrs 1357 . . . 4 ((((𝜑𝑥𝐴) ∧ 𝑦𝐵) ∧ 𝑧𝐶) → 𝜓)
32ralrimiva 3140 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → ∀𝑧𝐶 𝜓)
43ralrimiva 3140 . 2 ((𝜑𝑥𝐴) → ∀𝑦𝐵𝑧𝐶 𝜓)
54ralrimiva 3140 1 (𝜑 → ∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1084  wcel 2098  wral 3055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905
This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1086  df-ral 3056
This theorem is referenced by:  ispod  5590  swopolem  5591  isopolem  7338  caovassg  7602  caovcang  7605  caovordig  7609  caovordg  7611  caovdig  7618  caovdirg  7621  caofass  7704  caoftrn  7705  2oppccomf  17680  oppccomfpropd  17682  issubc3  17808  fthmon  17889  fuccocl  17929  fucidcl  17930  invfuc  17939  resssetc  18054  resscatc  18071  curf2cl  18196  yonedalem4c  18242  yonedalem3  18245  latdisdlem  18461  isrngd  20078  prdsrngd  20081  srgo2times  20117  srgcom4lem  20118  ringo2times  20174  ringcomlem  20178  isringd  20190  prdsringd  20220  islmodd  20712  islmhm2  20886  rnglidl1  21091  rnglidlmsgrp  21104  rnglidlrng  21105  isdomn4  21212  isphld  21547  ocvlss  21565  isassad  21759  mdetuni0  22478  mdetmul  22480  isngp4  24476  conway  27687  mulsprop  27985  tglowdim2ln  28410  f1otrgitv  28629  f1otrg  28630  f1otrge  28631  xmstrkgc  28651  eengtrkg  28752  eengtrkge  28753  submomnd  32734  ccfldsrarelvec  33264  isrngod  37279  rngomndo  37316  isgrpda  37336  islfld  38445  lfladdcl  38454  lflnegcl  38458  lshpkrcl  38499  lclkr  40917  lclkrs  40923  lcfr  40969  copissgrp  47123  cznrng  47216  topdlat  47908  catprs2  47911  idmon  47915  idepi  47916  thincmon  47933  thincepi  47934  isthincd2  47937  grptcmon  47995  grptcepi  47996
  Copyright terms: Public domain W3C validator