Theorem ralrimivvva 3194

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   ∈ wcel 2114  ∀wral 3140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085  df-ral 3145

This theorem is referenced by:  ispod  5484  swopolem  5485  isopolem  7100  caovassg  7348  caovcang  7351  caovordig  7355  caovordg  7357  caovdig  7364  caovdirg  7367  caofass  7445  caoftrn  7446  2oppccomf  16997  oppccomfpropd  16999  issubc3  17121  fthmon  17199  fuccocl  17236  fucidcl  17237  invfuc  17246  resssetc  17354  resscatc  17367  curf2cl  17483  yonedalem4c  17529  yonedalem3  17532  latdisdlem  17801  isringd  19337  prdsringd  19364  islmodd  19642  islmhm2  19812  isassad  20098  isphld  20800  ocvlss  20818  mdetuni0  21232  mdetmul  21234  isngp4  23223  tglowdim2ln  26439  f1otrgitv  26658  f1otrg  26659  f1otrge  26660  xmstrkgc  26674  eengtrkg  26774  eengtrkge  26775  submomnd  30713  ccfldsrarelvec  31058  conway  33266  isrngod  35178  rngomndo  35215  isgrpda  35235  islfld  36200  lfladdcl  36209  lflnegcl  36213  lshpkrcl  36254  lclkr  38671  lclkrs  38677  lcfr  38723  copissgrp  44082  lidlmsgrp  44204  lidlrng  44205  cznrng  44233