Theorem ralrimivvva 3203

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2106  ∀wral 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ral 3060

This theorem is referenced by:  ispod  5606  swopolem  5607  isopolem  7365  caovassg  7631  caovcang  7634  caovordig  7638  caovordg  7640  caovdig  7647  caovdirg  7650  caofass  7736  caoftrn  7737  2oppccomf  17772  oppccomfpropd  17774  issubc3  17900  fthmon  17981  fuccocl  18021  fucidcl  18022  invfuc  18031  resssetc  18146  resscatc  18163  curf2cl  18288  yonedalem4c  18334  yonedalem3  18337  latdisdlem  18554  isrngd  20191  prdsrngd  20194  srgo2times  20230  srgcom4lem  20231  ringo2times  20289  ringcomlem  20293  isringd  20305  prdsringd  20335  isdomn4  20733  islmodd  20881  islmhm2  21055  rnglidl1  21260  rnglidlmsgrp  21274  rnglidlrng  21275  isphld  21690  ocvlss  21708  isassad  21903  mdetuni0  22643  mdetmul  22645  isngp4  24641  conway  27859  mulsprop  28171  tglowdim2ln  28674  f1otrgitv  28893  f1otrg  28894  f1otrge  28895  xmstrkgc  28915  eengtrkg  29016  eengtrkge  29017  submomnd  33070  ccfldsrarelvec  33696  weiunpo  36448  isrngod  37885  rngomndo  37922  isgrpda  37942  islfld  39044  lfladdcl  39053  lflnegcl  39057  lshpkrcl  39098  lclkr  41516  lclkrs  41522  lcfr  41568  copissgrp  48012  cznrng  48105  topdlat  48793  catprs2  48801  idmon  48805  idepi  48806  thincmon  48834  thincepi  48835  isthincd2  48838  grptcmon  48902  grptcepi  48903