Theorem ralrimivvva 3210

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1099   ∈ wcel 2144  ∀wral 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1101  df-ral 3079

This theorem is referenced by:  ispod  5566  swopolem  5567  isopolem  7331  caovassg  7596  caovcang  7599  caovordig  7603  caovordg  7605  caovdig  7612  caovdirg  7615  caofass  7702  caoftrn  7703  2oppccomf  17759  oppccomfpropd  17761  issubc3  17884  fthmon  17964  fuccocl  18002  fucidcl  18003  invfuc  18012  resssetc  18127  resscatc  18144  curf2cl  18265  yonedalem4c  18311  yonedalem3  18314  latdisdlem  18530  submomnd  20174  isrngd  20221  prdsrngd  20224  srgo2times  20264  srgcom4lem  20265  ringo2times  20327  ringcomlem  20331  isringd  20343  prdsringd  20371  isdomn4  20768  islmodd  20935  islmhm2  21107  rnglidl1  21304  rnglidlmsgrp  21318  rnglidlrng  21319  isphld  21708  ocvlss  21726  isassad  21919  mdetuni0  22683  mdetmul  22685  isngp4  24674  conway  27874  mulsprop  28225  tglowdim2ln  28823  f1otrgitv  29072  f1otrg  29073  f1otrge  29074  xmstrkgc  29088  eengtrkg  29189  eengtrkge  29190  ccfldsrarelvec  33970  weiunpo  36830  isrngod  38402  rngomndo  38439  isgrpda  38459  islfld  39691  lfladdcl  39700  lflnegcl  39704  lshpkrcl  39745  lclkr  42162  lclkrs  42168  lcfr  42214  copissgrp  48795  cznrng  48888  topdlat  49630  catprs2  49638  idmon  49646  idepi  49647  ssccatid  49698  resccatlem  49699  fthcomf  49783  thincmon  50059  thincepi  50060  isthincd2  50063  oppcthinco  50065  oppcthinendcALT  50067  grptcmon  50219  grptcepi  50220