Theorem ralrimivvva 3181

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2109  ∀wral 3044

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 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ral 3045

This theorem is referenced by:  ispod  5548  swopolem  5549  isopolem  7302  caovassg  7567  caovcang  7570  caovordig  7574  caovordg  7576  caovdig  7583  caovdirg  7586  caofass  7673  caoftrn  7674  2oppccomf  17667  oppccomfpropd  17669  issubc3  17792  fthmon  17872  fuccocl  17910  fucidcl  17911  invfuc  17920  resssetc  18035  resscatc  18052  curf2cl  18173  yonedalem4c  18219  yonedalem3  18222  latdisdlem  18438  submomnd  20047  isrngd  20094  prdsrngd  20097  srgo2times  20133  srgcom4lem  20134  ringo2times  20196  ringcomlem  20200  isringd  20212  prdsringd  20242  isdomn4  20637  islmodd  20805  islmhm2  20978  rnglidl1  21175  rnglidlmsgrp  21189  rnglidlrng  21190  isphld  21597  ocvlss  21615  isassad  21808  mdetuni0  22542  mdetmul  22544  isngp4  24534  conway  27746  mulsprop  28074  tglowdim2ln  28632  f1otrgitv  28851  f1otrg  28852  f1otrge  28853  xmstrkgc  28867  eengtrkg  28967  eengtrkge  28968  ccfldsrarelvec  33660  weiunpo  36447  isrngod  37886  rngomndo  37923  isgrpda  37943  islfld  39049  lfladdcl  39058  lflnegcl  39062  lshpkrcl  39103  lclkr  41521  lclkrs  41527  lcfr  41573  copissgrp  48150  cznrng  48243  topdlat  48986  catprs2  48995  idmon  49003  idepi  49004  ssccatid  49055  resccatlem  49056  fthcomf  49140  thincmon  49416  thincepi  49417  isthincd2  49420  oppcthinco  49422  oppcthinendcALT  49424  grptcmon  49576  grptcepi  49577