Theorem ralrimivvva 3194

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

Step	Hyp	Ref	Expression
1		ralrimivvva.1	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) → 𝜓)
2	1	3anassrs 1357	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐶) → 𝜓)
3	2	ralrimiva 3136	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐶 𝜓)
4	3	ralrimiva 3136	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓)
5	4	ralrimiva 3136	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084   ∈ wcel 2098  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-ral 3052

This theorem is referenced by:  ispod  5593  swopolem  5594  isopolem  7348  caovassg  7615  caovcang  7618  caovordig  7622  caovordg  7624  caovdig  7631  caovdirg  7634  caofass  7719  caoftrn  7720  2oppccomf  17704  oppccomfpropd  17706  issubc3  17832  fthmon  17913  fuccocl  17953  fucidcl  17954  invfuc  17963  resssetc  18078  resscatc  18095  curf2cl  18220  yonedalem4c  18266  yonedalem3  18269  latdisdlem  18485  isrngd  20115  prdsrngd  20118  srgo2times  20154  srgcom4lem  20155  ringo2times  20213  ringcomlem  20217  isringd  20229  prdsringd  20259  islmodd  20751  islmhm2  20925  rnglidl1  21130  rnglidlmsgrp  21143  rnglidlrng  21144  isdomn4  21252  isphld  21588  ocvlss  21606  isassad  21800  mdetuni0  22539  mdetmul  22541  isngp4  24537  conway  27748  mulsprop  28050  tglowdim2ln  28497  f1otrgitv  28716  f1otrg  28717  f1otrge  28718  xmstrkgc  28738  eengtrkg  28839  eengtrkge  28840  submomnd  32833  ccfldsrarelvec  33415  isrngod  37427  rngomndo  37464  isgrpda  37484  islfld  38589  lfladdcl  38598  lflnegcl  38602  lshpkrcl  38643  lclkr  41061  lclkrs  41067  lcfr  41113  copissgrp  47341  cznrng  47434  topdlat  48126  catprs2  48129  idmon  48133  idepi  48134  thincmon  48151  thincepi  48152  isthincd2  48155  grptcmon  48213  grptcepi  48214