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  27710  mulsprop  28038  tglowdim2ln  28596  f1otrgitv  28815  f1otrg  28816  f1otrge  28817  xmstrkgc  28831  eengtrkg  28931  eengtrkge  28932  ccfldsrarelvec  33644  weiunpo  36449  isrngod  37888  rngomndo  37925  isgrpda  37945  islfld  39051  lfladdcl  39060  lflnegcl  39064  lshpkrcl  39105  lclkr  41522  lclkrs  41528  lcfr  41574  copissgrp  48162  cznrng  48255  topdlat  48998  catprs2  49007  idmon  49015  idepi  49016  ssccatid  49067  resccatlem  49068  fthcomf  49152  thincmon  49428  thincepi  49429  isthincd2  49432  oppcthinco  49434  oppcthinendcALT  49436  grptcmon  49588  grptcepi  49589