Theorem ralrimivvva 3208

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ral 3077

This theorem is used by:  ispod  5565  swopolem  5566  isopolem  7342  caovassg  7608  caovcang  7611  caovordig  7615  caovordg  7617  caovdig  7624  caovdirg  7627  caofass  7717  caoftrn  7718  2oppccomf  17846  oppccomfpropd  17848  issubc3  17971  fthmon  18051  fuccocl  18089  fucidcl  18090  invfuc  18099  resssetc  18214  resscatc  18231  curf2cl  18352  yonedalem4c  18398  yonedalem3  18401  latdisdlem  18617  submomnd  20293  isrngd  20342  prdsrngd  20345  srgo2times  20385  srgcom4lem  20386  ringo2times  20451  ringcomlem  20455  isringd  20469  prdsringd  20497  isdomn4  20914  islmodd  21088  islmhm2  21260  rnglidl1  21459  rnglidlmsgrp  21481  rnglidlrng  21482  isphld  21907  ocvlss  21925  isassad  22120  mdetuni0  22883  mdetmul  22885  isngp4  24878  conway  28084  mulsprop  28435  tglowdim2ln  29039  f1otrgitv  29366  f1otrg  29367  f1otrge  29368  xmstrkgc  29382  eengtrkg  29483  eengtrkge  29484  ccfldsrarelvec  34222  weiunpo  37169  isrngod  38746  rngomndo  38783  isgrpda  38803  islfld  40033  lfladdcl  40042  lflnegcl  40046  lshpkrcl  40087  lclkr  42504  lclkrs  42510  lcfr  42556  copissgrp  49181  cznrng  49274  topdlat  50028  catprs2  50036  idmon  50044  idepi  50045  ssccatid  50096  resccatlem  50097  fthcomf  50181  thincmon  50457  thincepi  50458  isthincd2  50461  oppcthinco  50463  oppcthinendcALT  50465  grptcmon  50617  grptcepi  50618