Theorem ralrimivvva 3201

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085   ∈ wcel 2104  ∀wral 3059

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 1911

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1087  df-ral 3060

This theorem is referenced by:  ispod  5596  swopolem  5597  isopolem  7344  caovassg  7607  caovcang  7610  caovordig  7614  caovordg  7616  caovdig  7623  caovdirg  7626  caofass  7709  caoftrn  7710  2oppccomf  17675  oppccomfpropd  17677  issubc3  17803  fthmon  17882  fuccocl  17921  fucidcl  17922  invfuc  17931  resssetc  18046  resscatc  18063  curf2cl  18188  yonedalem4c  18234  yonedalem3  18237  latdisdlem  18453  isrngd  20067  prdsrngd  20070  srgo2times  20106  srgcom4lem  20107  ringo2times  20163  ringcomlem  20167  isringd  20179  prdsringd  20209  islmodd  20620  islmhm2  20793  rnglidl1  21033  rnglidlmsgrp  21035  rnglidlrng  21036  isdomn4  21118  isphld  21426  ocvlss  21444  isassad  21638  mdetuni0  22343  mdetmul  22345  isngp4  24341  conway  27537  mulsprop  27825  tglowdim2ln  28169  f1otrgitv  28388  f1otrg  28389  f1otrge  28390  xmstrkgc  28410  eengtrkg  28511  eengtrkge  28512  submomnd  32498  ccfldsrarelvec  33034  isrngod  37069  rngomndo  37106  isgrpda  37126  islfld  38235  lfladdcl  38244  lflnegcl  38248  lshpkrcl  38289  lclkr  40707  lclkrs  40713  lcfr  40759  copissgrp  46844  cznrng  46941  topdlat  47716  catprs2  47719  idmon  47723  idepi  47724  thincmon  47741  thincepi  47742  isthincd2  47745  grptcmon  47803  grptcepi  47804