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

Theorem ralrimivvva 2955
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 1282 . . . 4 ((((𝜑𝑥𝐴) ∧ 𝑦𝐵) ∧ 𝑧𝐶) → 𝜓)
32ralrimiva 2949 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → ∀𝑧𝐶 𝜓)
43ralrimiva 2949 . 2 ((𝜑𝑥𝐴) → ∀𝑦𝐵𝑧𝐶 𝜓)
54ralrimiva 2949 1 (𝜑 → ∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1031  wcel 1977  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827
This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033  df-ral 2901
This theorem is referenced by:  ispod  4967  swopolem  4968  isopolem  6495  caovassg  6730  caovcang  6733  caovordig  6737  caovordg  6739  caovdig  6746  caovdirg  6749  caofass  6829  caoftrn  6830  2oppccomf  16208  oppccomfpropd  16210  issubc3  16332  fthmon  16410  fuccocl  16447  fucidcl  16448  invfuc  16457  resssetc  16565  resscatc  16578  curf2cl  16694  yonedalem4c  16740  yonedalem3  16743  latdisdlem  17012  isringd  18408  prdsringd  18435  islmodd  18692  islmhm2  18859  isassad  19144  isphld  19818  ocvlss  19835  mdetuni0  20246  mdetmul  20248  isngp4  22226  tglowdim2ln  25346  f1otrgitv  25550  f1otrg  25551  f1otrge  25552  xmstrkgc  25566  eengtrkg  25665  eengtrkge  25666  submomnd  29041  isrngod  32867  rngomndo  32904  isgrpda  32924  islfld  33367  lfladdcl  33376  lflnegcl  33380  lshpkrcl  33421  lclkr  35840  lclkrs  35846  lcfr  35892  copissgrp  41598  lidlmsgrp  41716  lidlrng  41717  cznrng  41747
  Copyright terms: Public domain W3C validator