Theorem ralrimivvva 3184

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

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

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 3046

This theorem is referenced by:  ispod  5558  swopolem  5559  isopolem  7323  caovassg  7590  caovcang  7593  caovordig  7597  caovordg  7599  caovdig  7606  caovdirg  7609  caofass  7696  caoftrn  7697  2oppccomf  17693  oppccomfpropd  17695  issubc3  17818  fthmon  17898  fuccocl  17936  fucidcl  17937  invfuc  17946  resssetc  18061  resscatc  18078  curf2cl  18199  yonedalem4c  18245  yonedalem3  18248  latdisdlem  18462  isrngd  20089  prdsrngd  20092  srgo2times  20128  srgcom4lem  20129  ringo2times  20191  ringcomlem  20195  isringd  20207  prdsringd  20237  isdomn4  20632  islmodd  20779  islmhm2  20952  rnglidl1  21149  rnglidlmsgrp  21163  rnglidlrng  21164  isphld  21570  ocvlss  21588  isassad  21781  mdetuni0  22515  mdetmul  22517  isngp4  24507  conway  27718  mulsprop  28040  tglowdim2ln  28585  f1otrgitv  28804  f1otrg  28805  f1otrge  28806  xmstrkgc  28820  eengtrkg  28920  eengtrkge  28921  submomnd  33031  ccfldsrarelvec  33673  weiunpo  36460  isrngod  37899  rngomndo  37936  isgrpda  37956  islfld  39062  lfladdcl  39071  lflnegcl  39075  lshpkrcl  39116  lclkr  41534  lclkrs  41540  lcfr  41586  copissgrp  48160  cznrng  48253  topdlat  48996  catprs2  49005  idmon  49013  idepi  49014  ssccatid  49065  resccatlem  49066  fthcomf  49150  thincmon  49426  thincepi  49427  isthincd2  49430  oppcthinco  49432  oppcthinendcALT  49434  grptcmon  49586  grptcepi  49587