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

Theorem ralrimivvva 3187
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 3177 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → ∀𝑧𝐶 𝜓)
43ralrimiva 3177 . 2 ((𝜑𝑥𝐴) → ∀𝑦𝐵𝑧𝐶 𝜓)
54ralrimiva 3177 1 (𝜑 → ∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084  wcel 2115  wral 3133
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ral 3138
This theorem is referenced by:  ispod  5469  swopolem  5470  isopolem  7091  caovassg  7340  caovcang  7343  caovordig  7347  caovordg  7349  caovdig  7356  caovdirg  7359  caofass  7437  caoftrn  7438  2oppccomf  16995  oppccomfpropd  16997  issubc3  17119  fthmon  17197  fuccocl  17234  fucidcl  17235  invfuc  17244  resssetc  17352  resscatc  17365  curf2cl  17481  yonedalem4c  17527  yonedalem3  17530  latdisdlem  17799  isringd  19338  prdsringd  19365  islmodd  19640  islmhm2  19810  isassad  20096  isphld  20798  ocvlss  20816  mdetuni0  21230  mdetmul  21232  isngp4  23221  tglowdim2ln  26448  f1otrgitv  26667  f1otrg  26668  f1otrge  26669  xmstrkgc  26683  eengtrkg  26783  eengtrkge  26784  submomnd  30743  ccfldsrarelvec  31116  conway  33321  isrngod  35281  rngomndo  35318  isgrpda  35338  islfld  36303  lfladdcl  36312  lflnegcl  36316  lshpkrcl  36357  lclkr  38774  lclkrs  38780  lcfr  38826  copissgrp  44354  lidlmsgrp  44476  lidlrng  44477  cznrng  44505
  Copyright terms: Public domain W3C validator