Theorem ralrimivvva 3175

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ral 3045

This theorem is referenced by:  ispod  5536  swopolem  5537  isopolem  7282  caovassg  7547  caovcang  7550  caovordig  7554  caovordg  7556  caovdig  7563  caovdirg  7566  caofass  7653  caoftrn  7654  2oppccomf  17631  oppccomfpropd  17633  issubc3  17756  fthmon  17836  fuccocl  17874  fucidcl  17875  invfuc  17884  resssetc  17999  resscatc  18016  curf2cl  18137  yonedalem4c  18183  yonedalem3  18186  latdisdlem  18402  submomnd  20011  isrngd  20058  prdsrngd  20061  srgo2times  20097  srgcom4lem  20098  ringo2times  20160  ringcomlem  20164  isringd  20176  prdsringd  20206  isdomn4  20601  islmodd  20769  islmhm2  20942  rnglidl1  21139  rnglidlmsgrp  21153  rnglidlrng  21154  isphld  21561  ocvlss  21579  isassad  21772  mdetuni0  22506  mdetmul  22508  isngp4  24498  conway  27711  mulsprop  28040  tglowdim2ln  28600  f1otrgitv  28819  f1otrg  28820  f1otrge  28821  xmstrkgc  28835  eengtrkg  28935  eengtrkge  28936  ccfldsrarelvec  33654  weiunpo  36459  isrngod  37898  rngomndo  37935  isgrpda  37955  islfld  39061  lfladdcl  39070  lflnegcl  39074  lshpkrcl  39115  lclkr  41532  lclkrs  41538  lcfr  41584  copissgrp  48172  cznrng  48265  topdlat  49008  catprs2  49017  idmon  49025  idepi  49026  ssccatid  49077  resccatlem  49078  fthcomf  49162  thincmon  49438  thincepi  49439  isthincd2  49442  oppcthinco  49444  oppcthinendcALT  49446  grptcmon  49598  grptcepi  49599