Theorem ralrimivvva 3157

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   ∈ wcel 2111  ∀wral 3106

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 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ral 3111

This theorem is referenced by:  ispod  5446  swopolem  5447  isopolem  7077  caovassg  7326  caovcang  7329  caovordig  7333  caovordg  7335  caovdig  7342  caovdirg  7345  caofass  7423  caoftrn  7424  2oppccomf  16987  oppccomfpropd  16989  issubc3  17111  fthmon  17189  fuccocl  17226  fucidcl  17227  invfuc  17236  resssetc  17344  resscatc  17357  curf2cl  17473  yonedalem4c  17519  yonedalem3  17522  latdisdlem  17791  isringd  19331  prdsringd  19358  islmodd  19633  islmhm2  19803  isphld  20343  ocvlss  20361  isassad  20553  mdetuni0  21226  mdetmul  21228  isngp4  23218  tglowdim2ln  26445  f1otrgitv  26664  f1otrg  26665  f1otrge  26666  xmstrkgc  26680  eengtrkg  26780  eengtrkge  26781  submomnd  30761  ccfldsrarelvec  31144  conway  33377  isrngod  35336  rngomndo  35373  isgrpda  35393  islfld  36358  lfladdcl  36367  lflnegcl  36371  lshpkrcl  36412  lclkr  38829  lclkrs  38835  lcfr  38881  copissgrp  44428  lidlmsgrp  44550  lidlrng  44551  cznrng  44579