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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114  ∀wral 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ral 3050

This theorem is referenced by:  ispod  5537  swopolem  5538  isopolem  7289  caovassg  7554  caovcang  7557  caovordig  7561  caovordg  7563  caovdig  7570  caovdirg  7573  caofass  7660  caoftrn  7661  2oppccomf  17680  oppccomfpropd  17682  issubc3  17805  fthmon  17885  fuccocl  17923  fucidcl  17924  invfuc  17933  resssetc  18048  resscatc  18065  curf2cl  18186  yonedalem4c  18232  yonedalem3  18235  latdisdlem  18451  submomnd  20096  isrngd  20143  prdsrngd  20146  srgo2times  20182  srgcom4lem  20183  ringo2times  20245  ringcomlem  20249  isringd  20261  prdsringd  20289  isdomn4  20682  islmodd  20850  islmhm2  21022  rnglidl1  21219  rnglidlmsgrp  21233  rnglidlrng  21234  isphld  21623  ocvlss  21641  isassad  21834  mdetuni0  22574  mdetmul  22576  isngp4  24565  conway  27759  mulsprop  28110  tglowdim2ln  28707  f1otrgitv  28926  f1otrg  28927  f1otrge  28928  xmstrkgc  28942  eengtrkg  29043  eengtrkge  29044  ccfldsrarelvec  33803  weiunpo  36635  isrngod  38207  rngomndo  38244  isgrpda  38264  islfld  39496  lfladdcl  39505  lflnegcl  39509  lshpkrcl  39550  lclkr  41967  lclkrs  41973  lcfr  42019  copissgrp  48632  cznrng  48725  topdlat  49467  catprs2  49475  idmon  49483  idepi  49484  ssccatid  49535  resccatlem  49536  fthcomf  49620  thincmon  49896  thincepi  49897  isthincd2  49900  oppcthinco  49902  oppcthinendcALT  49904  grptcmon  50056  grptcepi  50057