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

Theorem ralrimivvva 3121
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 1453 . . . 4 ((((𝜑𝑥𝐴) ∧ 𝑦𝐵) ∧ 𝑧𝐶) → 𝜓)
32ralrimiva 3115 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → ∀𝑧𝐶 𝜓)
43ralrimiva 3115 . 2 ((𝜑𝑥𝐴) → ∀𝑦𝐵𝑧𝐶 𝜓)
54ralrimiva 3115 1 (𝜑 → ∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071  wcel 2145  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991
This theorem depends on definitions:  df-bi 197  df-an 383  df-3an 1073  df-ral 3066
This theorem is referenced by:  ispod  5179  swopolem  5180  isopolem  6741  caovassg  6983  caovcang  6986  caovordig  6990  caovordg  6992  caovdig  6999  caovdirg  7002  caofass  7082  caoftrn  7083  2oppccomf  16592  oppccomfpropd  16594  issubc3  16716  fthmon  16794  fuccocl  16831  fucidcl  16832  invfuc  16841  resssetc  16949  resscatc  16962  curf2cl  17079  yonedalem4c  17125  yonedalem3  17128  latdisdlem  17397  isringd  18793  prdsringd  18820  islmodd  19079  islmhm2  19251  isassad  19538  isphld  20216  ocvlss  20233  mdetuni0  20645  mdetmul  20647  isngp4  22636  tglowdim2ln  25767  f1otrgitv  25971  f1otrg  25972  f1otrge  25973  xmstrkgc  25987  eengtrkg  26086  eengtrkge  26087  submomnd  30050  conway  32247  isrngod  34029  rngomndo  34066  isgrpda  34086  islfld  34871  lfladdcl  34880  lflnegcl  34884  lshpkrcl  34925  lclkr  37343  lclkrs  37349  lcfr  37395  copissgrp  42333  lidlmsgrp  42451  lidlrng  42452  cznrng  42480
  Copyright terms: Public domain W3C validator