Theorem ralrimivvva 3136

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068   ∈ wcel 2050  ∀wral 3082

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869

This theorem depends on definitions:  df-bi 199  df-an 388  df-3an 1070  df-ral 3087

This theorem is referenced by:  ispod  5328  swopolem  5329  isopolem  6915  caovassg  7156  caovcang  7159  caovordig  7163  caovordg  7165  caovdig  7172  caovdirg  7175  caofass  7255  caoftrn  7256  2oppccomf  16847  oppccomfpropd  16849  issubc3  16971  fthmon  17049  fuccocl  17086  fucidcl  17087  invfuc  17096  resssetc  17204  resscatc  17217  curf2cl  17333  yonedalem4c  17379  yonedalem3  17382  latdisdlem  17651  isringd  19052  prdsringd  19079  islmodd  19356  islmhm2  19526  isassad  19811  isphld  20494  ocvlss  20512  mdetuni0  20928  mdetmul  20930  isngp4  22918  tglowdim2ln  26133  f1otrgitv  26353  f1otrg  26354  f1otrge  26355  xmstrkgc  26369  eengtrkg  26469  eengtrkge  26470  submomnd  30429  ccfldsrarelvec  30685  conway  32785  isrngod  34618  rngomndo  34655  isgrpda  34675  islfld  35643  lfladdcl  35652  lflnegcl  35656  lshpkrcl  35697  lclkr  38114  lclkrs  38120  lcfr  38166  copissgrp  43443  lidlmsgrp  43561  lidlrng  43562  cznrng  43590