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

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

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 3051

This theorem is referenced by:  ispod  5540  swopolem  5541  isopolem  7291  caovassg  7556  caovcang  7559  caovordig  7563  caovordg  7565  caovdig  7572  caovdirg  7575  caofass  7662  caoftrn  7663  2oppccomf  17650  oppccomfpropd  17652  issubc3  17775  fthmon  17855  fuccocl  17893  fucidcl  17894  invfuc  17903  resssetc  18018  resscatc  18035  curf2cl  18156  yonedalem4c  18202  yonedalem3  18205  latdisdlem  18421  submomnd  20063  isrngd  20110  prdsrngd  20113  srgo2times  20149  srgcom4lem  20150  ringo2times  20212  ringcomlem  20216  isringd  20228  prdsringd  20258  isdomn4  20651  islmodd  20819  islmhm2  20992  rnglidl1  21189  rnglidlmsgrp  21203  rnglidlrng  21204  isphld  21611  ocvlss  21629  isassad  21822  mdetuni0  22567  mdetmul  22569  isngp4  24558  conway  27775  mulsprop  28110  tglowdim2ln  28704  f1otrgitv  28923  f1otrg  28924  f1otrge  28925  xmstrkgc  28939  eengtrkg  29040  eengtrkge  29041  ccfldsrarelvec  33807  weiunpo  36638  isrngod  38068  rngomndo  38105  isgrpda  38125  islfld  39357  lfladdcl  39366  lflnegcl  39370  lshpkrcl  39411  lclkr  41828  lclkrs  41834  lcfr  41880  copissgrp  48451  cznrng  48544  topdlat  49286  catprs2  49294  idmon  49302  idepi  49303  ssccatid  49354  resccatlem  49355  fthcomf  49439  thincmon  49715  thincepi  49716  isthincd2  49719  oppcthinco  49721  oppcthinendcALT  49723  grptcmon  49875  grptcepi  49876