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

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

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 3053

This theorem is referenced by:  ispod  5551  swopolem  5552  isopolem  7303  caovassg  7568  caovcang  7571  caovordig  7575  caovordg  7577  caovdig  7584  caovdirg  7587  caofass  7674  caoftrn  7675  2oppccomf  17662  oppccomfpropd  17664  issubc3  17787  fthmon  17867  fuccocl  17905  fucidcl  17906  invfuc  17915  resssetc  18030  resscatc  18047  curf2cl  18168  yonedalem4c  18214  yonedalem3  18217  latdisdlem  18433  submomnd  20078  isrngd  20125  prdsrngd  20128  srgo2times  20164  srgcom4lem  20165  ringo2times  20227  ringcomlem  20231  isringd  20243  prdsringd  20273  isdomn4  20666  islmodd  20834  islmhm2  21007  rnglidl1  21204  rnglidlmsgrp  21218  rnglidlrng  21219  isphld  21626  ocvlss  21644  isassad  21837  mdetuni0  22582  mdetmul  22584  isngp4  24573  conway  27792  mulsprop  28143  tglowdim2ln  28741  f1otrgitv  28960  f1otrg  28961  f1otrge  28962  xmstrkgc  28976  eengtrkg  29077  eengtrkge  29078  ccfldsrarelvec  33855  weiunpo  36687  isrngod  38178  rngomndo  38215  isgrpda  38235  islfld  39467  lfladdcl  39476  lflnegcl  39480  lshpkrcl  39521  lclkr  41938  lclkrs  41944  lcfr  41990  copissgrp  48557  cznrng  48650  topdlat  49392  catprs2  49400  idmon  49408  idepi  49409  ssccatid  49460  resccatlem  49461  fthcomf  49545  thincmon  49821  thincepi  49822  isthincd2  49825  oppcthinco  49827  oppcthinendcALT  49829  grptcmon  49981  grptcepi  49982