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

Theorem ralrimivvva 3001
 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 1313 . . . 4 ((((𝜑𝑥𝐴) ∧ 𝑦𝐵) ∧ 𝑧𝐶) → 𝜓)
32ralrimiva 2995 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → ∀𝑧𝐶 𝜓)
43ralrimiva 2995 . 2 ((𝜑𝑥𝐴) → ∀𝑦𝐵𝑧𝐶 𝜓)
54ralrimiva 2995 1 (𝜑 → ∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054   ∈ wcel 2030  ∀wral 2941 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879 This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1056  df-ral 2946 This theorem is referenced by:  ispod  5072  swopolem  5073  isopolem  6635  caovassg  6874  caovcang  6877  caovordig  6881  caovordg  6883  caovdig  6890  caovdirg  6893  caofass  6973  caoftrn  6974  2oppccomf  16432  oppccomfpropd  16434  issubc3  16556  fthmon  16634  fuccocl  16671  fucidcl  16672  invfuc  16681  resssetc  16789  resscatc  16802  curf2cl  16918  yonedalem4c  16964  yonedalem3  16967  latdisdlem  17236  isringd  18631  prdsringd  18658  islmodd  18917  islmhm2  19086  isassad  19371  isphld  20047  ocvlss  20064  mdetuni0  20475  mdetmul  20477  isngp4  22463  tglowdim2ln  25591  f1otrgitv  25795  f1otrg  25796  f1otrge  25797  xmstrkgc  25811  eengtrkg  25910  eengtrkge  25911  submomnd  29838  conway  32035  isrngod  33827  rngomndo  33864  isgrpda  33884  islfld  34667  lfladdcl  34676  lflnegcl  34680  lshpkrcl  34721  lclkr  37139  lclkrs  37145  lcfr  37191  copissgrp  42133  lidlmsgrp  42251  lidlrng  42252  cznrng  42280
 Copyright terms: Public domain W3C validator