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

Theorem ralrimivvva 3201
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 3143 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → ∀𝑧𝐶 𝜓)
43ralrimiva 3143 . 2 ((𝜑𝑥𝐴) → ∀𝑦𝐵𝑧𝐶 𝜓)
54ralrimiva 3143 1 (𝜑 → ∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084  wcel 2098  wral 3058
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 395  df-3an 1086  df-ral 3059
This theorem is referenced by:  ispod  5603  swopolem  5604  isopolem  7359  caovassg  7625  caovcang  7628  caovordig  7632  caovordg  7634  caovdig  7641  caovdirg  7644  caofass  7728  caoftrn  7729  2oppccomf  17714  oppccomfpropd  17716  issubc3  17842  fthmon  17923  fuccocl  17963  fucidcl  17964  invfuc  17973  resssetc  18088  resscatc  18105  curf2cl  18230  yonedalem4c  18276  yonedalem3  18279  latdisdlem  18495  isrngd  20120  prdsrngd  20123  srgo2times  20159  srgcom4lem  20160  ringo2times  20218  ringcomlem  20222  isringd  20234  prdsringd  20264  islmodd  20756  islmhm2  20930  rnglidl1  21135  rnglidlmsgrp  21148  rnglidlrng  21149  isdomn4  21257  isphld  21593  ocvlss  21611  isassad  21805  mdetuni0  22543  mdetmul  22545  isngp4  24541  conway  27752  mulsprop  28050  tglowdim2ln  28475  f1otrgitv  28694  f1otrg  28695  f1otrge  28696  xmstrkgc  28716  eengtrkg  28817  eengtrkge  28818  submomnd  32811  ccfldsrarelvec  33392  isrngod  37404  rngomndo  37441  isgrpda  37461  islfld  38566  lfladdcl  38575  lflnegcl  38579  lshpkrcl  38620  lclkr  41038  lclkrs  41044  lcfr  41090  copissgrp  47308  cznrng  47401  topdlat  48093  catprs2  48096  idmon  48100  idepi  48101  thincmon  48118  thincepi  48119  isthincd2  48122  grptcmon  48180  grptcepi  48181
  Copyright terms: Public domain W3C validator