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

Theorem ralrimivvva 3205
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 1361 . . . 4 ((((𝜑𝑥𝐴) ∧ 𝑦𝐵) ∧ 𝑧𝐶) → 𝜓)
32ralrimiva 3146 . . 3 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → ∀𝑧𝐶 𝜓)
43ralrimiva 3146 . 2 ((𝜑𝑥𝐴) → ∀𝑦𝐵𝑧𝐶 𝜓)
54ralrimiva 3146 1 (𝜑 → ∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087  wcel 2108  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ral 3062
This theorem is referenced by:  ispod  5601  swopolem  5602  isopolem  7365  caovassg  7631  caovcang  7634  caovordig  7638  caovordg  7640  caovdig  7647  caovdirg  7650  caofass  7737  caoftrn  7738  2oppccomf  17768  oppccomfpropd  17770  issubc3  17894  fthmon  17974  fuccocl  18012  fucidcl  18013  invfuc  18022  resssetc  18137  resscatc  18154  curf2cl  18276  yonedalem4c  18322  yonedalem3  18325  latdisdlem  18541  isrngd  20170  prdsrngd  20173  srgo2times  20209  srgcom4lem  20210  ringo2times  20272  ringcomlem  20276  isringd  20288  prdsringd  20318  isdomn4  20716  islmodd  20864  islmhm2  21037  rnglidl1  21242  rnglidlmsgrp  21256  rnglidlrng  21257  isphld  21672  ocvlss  21690  isassad  21885  mdetuni0  22627  mdetmul  22629  isngp4  24625  conway  27844  mulsprop  28156  tglowdim2ln  28659  f1otrgitv  28878  f1otrg  28879  f1otrge  28880  xmstrkgc  28900  eengtrkg  29001  eengtrkge  29002  submomnd  33087  ccfldsrarelvec  33721  weiunpo  36466  isrngod  37905  rngomndo  37942  isgrpda  37962  islfld  39063  lfladdcl  39072  lflnegcl  39076  lshpkrcl  39117  lclkr  41535  lclkrs  41541  lcfr  41587  copissgrp  48084  cznrng  48177  topdlat  48893  catprs2  48901  idmon  48908  idepi  48909  thincmon  49082  thincepi  49083  isthincd2  49086  oppcthinco  49088  oppcthinendcALT  49090  grptcmon  49190  grptcepi  49191
  Copyright terms: Public domain W3C validator