Theorem ralrimivvva 3181

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

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

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 3045

This theorem is referenced by:  ispod  5548  swopolem  5549  isopolem  7302  caovassg  7567  caovcang  7570  caovordig  7574  caovordg  7576  caovdig  7583  caovdirg  7586  caofass  7673  caoftrn  7674  2oppccomf  17666  oppccomfpropd  17668  issubc3  17791  fthmon  17871  fuccocl  17909  fucidcl  17910  invfuc  17919  resssetc  18034  resscatc  18051  curf2cl  18172  yonedalem4c  18218  yonedalem3  18221  latdisdlem  18437  submomnd  20046  isrngd  20093  prdsrngd  20096  srgo2times  20132  srgcom4lem  20133  ringo2times  20195  ringcomlem  20199  isringd  20211  prdsringd  20241  isdomn4  20636  islmodd  20804  islmhm2  20977  rnglidl1  21174  rnglidlmsgrp  21188  rnglidlrng  21189  isphld  21596  ocvlss  21614  isassad  21807  mdetuni0  22541  mdetmul  22543  isngp4  24533  conway  27745  mulsprop  28073  tglowdim2ln  28631  f1otrgitv  28850  f1otrg  28851  f1otrge  28852  xmstrkgc  28866  eengtrkg  28966  eengtrkge  28967  ccfldsrarelvec  33659  weiunpo  36446  isrngod  37885  rngomndo  37922  isgrpda  37942  islfld  39048  lfladdcl  39057  lflnegcl  39061  lshpkrcl  39102  lclkr  41520  lclkrs  41526  lcfr  41572  copissgrp  48149  cznrng  48242  topdlat  48985  catprs2  48994  idmon  49002  idepi  49003  ssccatid  49054  resccatlem  49055  fthcomf  49139  thincmon  49415  thincepi  49416  isthincd2  49419  oppcthinco  49421  oppcthinendcALT  49423  grptcmon  49575  grptcepi  49576