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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084   ∈ wcel 2098  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-ral 3059

This theorem is referenced by:  ispod  5603  swopolem  5604  isopolem  7359  caovassg  7625  caovcang  7628  caovordig  7632  caovordg  7634  caovdig  7641  caovdirg  7644  caofass  7728  caoftrn  7729  2oppccomf  17714  oppccomfpropd  17716  issubc3  17842  fthmon  17923  fuccocl  17963  fucidcl  17964  invfuc  17973  resssetc  18088  resscatc  18105  curf2cl  18230  yonedalem4c  18276  yonedalem3  18279  latdisdlem  18495  isrngd  20120  prdsrngd  20123  srgo2times  20159  srgcom4lem  20160  ringo2times  20218  ringcomlem  20222  isringd  20234  prdsringd  20264  islmodd  20756  islmhm2  20930  rnglidl1  21135  rnglidlmsgrp  21148  rnglidlrng  21149  isdomn4  21257  isphld  21593  ocvlss  21611  isassad  21805  mdetuni0  22543  mdetmul  22545  isngp4  24541  conway  27752  mulsprop  28050  tglowdim2ln  28475  f1otrgitv  28694  f1otrg  28695  f1otrge  28696  xmstrkgc  28716  eengtrkg  28817  eengtrkge  28818  submomnd  32811  ccfldsrarelvec  33392  isrngod  37404  rngomndo  37441  isgrpda  37461  islfld  38566  lfladdcl  38575  lflnegcl  38579  lshpkrcl  38620  lclkr  41038  lclkrs  41044  lcfr  41090  copissgrp  47308  cznrng  47401  topdlat  48093  catprs2  48096  idmon  48100  idepi  48101  thincmon  48118  thincepi  48119  isthincd2  48122  grptcmon  48180  grptcepi  48181