Theorem ralrimivvva 3127

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086   ∈ wcel 2106  ∀wral 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088  df-ral 3069

This theorem is referenced by:  ispod  5512  swopolem  5513  isopolem  7216  caovassg  7470  caovcang  7473  caovordig  7477  caovordg  7479  caovdig  7486  caovdirg  7489  caofass  7570  caoftrn  7571  2oppccomf  17436  oppccomfpropd  17438  issubc3  17564  fthmon  17643  fuccocl  17682  fucidcl  17683  invfuc  17692  resssetc  17807  resscatc  17824  curf2cl  17949  yonedalem4c  17995  yonedalem3  17998  latdisdlem  18214  isringd  19824  prdsringd  19851  islmodd  20129  islmhm2  20300  isphld  20859  ocvlss  20877  isassad  21071  mdetuni0  21770  mdetmul  21772  isngp4  23768  tglowdim2ln  27012  f1otrgitv  27231  f1otrg  27232  f1otrge  27233  xmstrkgc  27253  eengtrkg  27354  eengtrkge  27355  submomnd  31336  ccfldsrarelvec  31741  conway  33993  isrngod  36056  rngomndo  36093  isgrpda  36113  islfld  37076  lfladdcl  37085  lflnegcl  37089  lshpkrcl  37130  lclkr  39547  lclkrs  39553  lcfr  39599  isdomn4  40172  copissgrp  45362  lidlmsgrp  45484  lidlrng  45485  cznrng  45513  topdlat  46290  catprs2  46293  idmon  46297  idepi  46298  thincmon  46315  thincepi  46316  isthincd2  46319  grptcmon  46377  grptcepi  46378