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

Theorem ralrimivvva 3136
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 1340 . . . 4 ((((𝜑𝑥𝐴) ∧ 𝑦𝐵) ∧ 𝑧𝐶) → 𝜓)
32ralrimiva 3126 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → ∀𝑧𝐶 𝜓)
43ralrimiva 3126 . 2 ((𝜑𝑥𝐴) → ∀𝑦𝐵𝑧𝐶 𝜓)
54ralrimiva 3126 1 (𝜑 → ∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  w3a 1068  wcel 2050  wral 3082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869
This theorem depends on definitions:  df-bi 199  df-an 388  df-3an 1070  df-ral 3087
This theorem is referenced by:  ispod  5328  swopolem  5329  isopolem  6915  caovassg  7156  caovcang  7159  caovordig  7163  caovordg  7165  caovdig  7172  caovdirg  7175  caofass  7255  caoftrn  7256  2oppccomf  16847  oppccomfpropd  16849  issubc3  16971  fthmon  17049  fuccocl  17086  fucidcl  17087  invfuc  17096  resssetc  17204  resscatc  17217  curf2cl  17333  yonedalem4c  17379  yonedalem3  17382  latdisdlem  17651  isringd  19052  prdsringd  19079  islmodd  19356  islmhm2  19526  isassad  19811  isphld  20494  ocvlss  20512  mdetuni0  20928  mdetmul  20930  isngp4  22918  tglowdim2ln  26133  f1otrgitv  26353  f1otrg  26354  f1otrge  26355  xmstrkgc  26369  eengtrkg  26469  eengtrkge  26470  submomnd  30429  ccfldsrarelvec  30685  conway  32785  isrngod  34618  rngomndo  34655  isgrpda  34675  islfld  35643  lfladdcl  35652  lflnegcl  35656  lshpkrcl  35697  lclkr  38114  lclkrs  38120  lcfr  38166  copissgrp  43443  lidlmsgrp  43561  lidlrng  43562  cznrng  43590
  Copyright terms: Public domain W3C validator