Theorem ralrimivvva 3191

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 1361	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐶) → 𝜓)
3	2	ralrimiva 3133	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐶 𝜓)
4	3	ralrimiva 3133	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓)
5	4	ralrimiva 3133	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2109  ∀wral 3052

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 1088  df-ral 3053

This theorem is referenced by:  ispod  5575  swopolem  5576  isopolem  7343  caovassg  7610  caovcang  7613  caovordig  7617  caovordg  7619  caovdig  7626  caovdirg  7629  caofass  7716  caoftrn  7717  2oppccomf  17742  oppccomfpropd  17744  issubc3  17867  fthmon  17947  fuccocl  17985  fucidcl  17986  invfuc  17995  resssetc  18110  resscatc  18127  curf2cl  18248  yonedalem4c  18294  yonedalem3  18297  latdisdlem  18511  isrngd  20138  prdsrngd  20141  srgo2times  20177  srgcom4lem  20178  ringo2times  20240  ringcomlem  20244  isringd  20256  prdsringd  20286  isdomn4  20681  islmodd  20828  islmhm2  21001  rnglidl1  21198  rnglidlmsgrp  21212  rnglidlrng  21213  isphld  21619  ocvlss  21637  isassad  21830  mdetuni0  22564  mdetmul  22566  isngp4  24556  conway  27768  mulsprop  28090  tglowdim2ln  28635  f1otrgitv  28854  f1otrg  28855  f1otrge  28856  xmstrkgc  28870  eengtrkg  28970  eengtrkge  28971  submomnd  33083  ccfldsrarelvec  33717  weiunpo  36488  isrngod  37927  rngomndo  37964  isgrpda  37984  islfld  39085  lfladdcl  39094  lflnegcl  39098  lshpkrcl  39139  lclkr  41557  lclkrs  41563  lcfr  41609  copissgrp  48110  cznrng  48203  topdlat  48945  catprs2  48954  idmon  48962  idepi  48963  ssccatid  49006  resccatlem  49007  fthcomf  49064  thincmon  49286  thincepi  49287  isthincd2  49290  oppcthinco  49292  oppcthinendcALT  49294  grptcmon  49437  grptcepi  49438