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

Theorem ralrimivvva 2954
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 1281 . . . 4 ((((𝜑𝑥𝐴) ∧ 𝑦𝐵) ∧ 𝑧𝐶) → 𝜓)
32ralrimiva 2948 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → ∀𝑧𝐶 𝜓)
43ralrimiva 2948 . 2 ((𝜑𝑥𝐴) → ∀𝑦𝐵𝑧𝐶 𝜓)
54ralrimiva 2948 1 (𝜑 → ∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030  wcel 1976  wral 2895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-an 384  df-3an 1032  df-ral 2900
This theorem is referenced by:  ispod  4957  swopolem  4958  isopolem  6473  caovassg  6707  caovcang  6710  caovordig  6714  caovordg  6716  caovdig  6723  caovdirg  6726  caofass  6806  caoftrn  6807  2oppccomf  16154  oppccomfpropd  16156  issubc3  16278  fthmon  16356  fuccocl  16393  fucidcl  16394  invfuc  16403  resssetc  16511  resscatc  16524  curf2cl  16640  yonedalem4c  16686  yonedalem3  16689  latdisdlem  16958  isringd  18354  prdsringd  18381  islmodd  18638  islmhm2  18805  isassad  19090  isphld  19763  ocvlss  19777  mdetuni0  20188  mdetmul  20190  isngp4  22166  tglowdim2ln  25264  f1otrgitv  25468  f1otrg  25469  f1otrge  25470  xmstrkgc  25484  eengtrkg  25583  eengtrkge  25584  submomnd  28847  isrngod  32670  rngomndo  32707  isgrpda  32727  islfld  33170  lfladdcl  33179  lflnegcl  33183  lshpkrcl  33224  lclkr  35643  lclkrs  35649  lcfr  35695  copissgrp  41600  lidlmsgrp  41718  lidlrng  41719  cznrng  41749
  Copyright terms: Public domain W3C validator