Theorem ralrimivvva 3212

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

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

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 1945

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

This theorem is used by:  ispod  5572  swopolem  5573  isopolem  7373  caovassg  7640  caovcang  7643  caovordig  7647  caovordg  7649  caovdig  7656  caovdirg  7659  caofass  7754  caoftrn  7755  2oppccomf  17925  oppccomfpropd  17927  issubc3  18050  fthmon  18130  fuccocl  18168  fucidcl  18169  invfuc  18178  resssetc  18293  resscatc  18310  curf2cl  18431  yonedalem4c  18477  yonedalem3  18480  latdisdlem  18696  submomnd  20373  isrngd  20422  prdsrngd  20425  srgo2times  20465  srgcom4lem  20466  ringo2times  20531  ringcomlem  20535  isringd  20549  prdsringd  20577  isdomn4  20994  islmodd  21168  islmhm2  21340  rnglidl1  21539  rnglidlmsgrp  21561  rnglidlrng  21562  isphld  21987  ocvlss  22005  isassad  22200  mdetuni0  22963  mdetmul  22965  isngp4  24958  conway  28192  mulsprop  28543  tglowdim2ln  29147  f1otrgitv  29474  f1otrg  29475  f1otrge  29476  xmstrkgc  29490  eengtrkg  29591  eengtrkge  29592  ccfldsrarelvec  34370  weiunpo  37430  isrngod  39023  rngomndo  39060  isgrpda  39080  islfld  40310  lfladdcl  40319  lflnegcl  40323  lshpkrcl  40364  lclkr  42781  lclkrs  42787  lcfr  42833  copissgrp  49468  cznrng  49561  topdlat  50321  catprs2  50329  idmon  50337  idepi  50338  ssccatid  50389  resccatlem  50390  fthcomf  50476  thincmon  50771  thincepi  50772  isthincd2  50775  oppcthinco  50777  oppcthinendcALT  50779  grptcmon  50934  grptcepi  50935