Theorem ralrimivvva 3217

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-ral 3086

This theorem is referenced by:  ispod  5576  swopolem  5577  isopolem  7341  caovassg  7606  caovcang  7609  caovordig  7613  caovordg  7615  caovdig  7622  caovdirg  7625  caofass  7712  caoftrn  7713  2oppccomf  17777  oppccomfpropd  17779  issubc3  17902  fthmon  17982  fuccocl  18020  fucidcl  18021  invfuc  18030  resssetc  18145  resscatc  18162  curf2cl  18283  yonedalem4c  18329  yonedalem3  18332  latdisdlem  18548  submomnd  20198  isrngd  20247  prdsrngd  20250  srgo2times  20290  srgcom4lem  20291  ringo2times  20354  ringcomlem  20358  isringd  20370  prdsringd  20398  isdomn4  20796  islmodd  20961  islmhm2  21133  rnglidl1  21332  rnglidlmsgrp  21350  rnglidlrng  21351  isphld  21769  ocvlss  21787  isassad  21980  mdetuni0  22743  mdetmul  22745  isngp4  24734  conway  27934  mulsprop  28285  tglowdim2ln  28883  f1otrgitv  29156  f1otrg  29157  f1otrge  29158  xmstrkgc  29172  eengtrkg  29273  eengtrkge  29274  ccfldsrarelvec  34002  weiunpo  36861  isrngod  38432  rngomndo  38469  isgrpda  38489  islfld  39721  lfladdcl  39730  lflnegcl  39734  lshpkrcl  39775  lclkr  42192  lclkrs  42198  lcfr  42244  copissgrp  48815  cznrng  48908  topdlat  49660  catprs2  49668  idmon  49676  idepi  49677  ssccatid  49728  resccatlem  49729  fthcomf  49813  thincmon  50089  thincepi  50090  isthincd2  50093  oppcthinco  50095  oppcthinendcALT  50097  grptcmon  50249  grptcepi  50250