Theorem ralrimivvva 3187

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093   ∈ wcel 2121  ∀wral 3055

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

This theorem depends on definitions:  df-bi 209  df-an 398  df-3an 1095  df-ral 3056

This theorem is referenced by:  ispod  5538  swopolem  5539  isopolem  7293  caovassg  7558  caovcang  7561  caovordig  7565  caovordg  7567  caovdig  7574  caovdirg  7577  caofass  7664  caoftrn  7665  2oppccomf  17686  oppccomfpropd  17688  issubc3  17811  fthmon  17891  fuccocl  17929  fucidcl  17930  invfuc  17939  resssetc  18054  resscatc  18071  curf2cl  18192  yonedalem4c  18238  yonedalem3  18241  latdisdlem  18457  submomnd  20102  isrngd  20149  prdsrngd  20152  srgo2times  20188  srgcom4lem  20189  ringo2times  20251  ringcomlem  20255  isringd  20267  prdsringd  20295  isdomn4  20692  islmodd  20860  islmhm2  21032  rnglidl1  21229  rnglidlmsgrp  21243  rnglidlrng  21244  isphld  21633  ocvlss  21651  isassad  21844  mdetuni0  22608  mdetmul  22610  isngp4  24599  conway  27793  mulsprop  28144  tglowdim2ln  28741  f1otrgitv  28960  f1otrg  28961  f1otrge  28962  xmstrkgc  28976  eengtrkg  29077  eengtrkge  29078  ccfldsrarelvec  33867  weiunpo  36708  isrngod  38280  rngomndo  38317  isgrpda  38337  islfld  39569  lfladdcl  39578  lflnegcl  39582  lshpkrcl  39623  lclkr  42040  lclkrs  42046  lcfr  42092  copissgrp  48673  cznrng  48766  topdlat  49508  catprs2  49516  idmon  49524  idepi  49525  ssccatid  49576  resccatlem  49577  fthcomf  49661  thincmon  49937  thincepi  49938  isthincd2  49941  oppcthinco  49943  oppcthinendcALT  49945  grptcmon  50097  grptcepi  50098