Theorem ralrimivvva 3205

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2108  ∀wral 3061

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 1089  df-ral 3062

This theorem is referenced by:  ispod  5601  swopolem  5602  isopolem  7365  caovassg  7631  caovcang  7634  caovordig  7638  caovordg  7640  caovdig  7647  caovdirg  7650  caofass  7737  caoftrn  7738  2oppccomf  17768  oppccomfpropd  17770  issubc3  17894  fthmon  17974  fuccocl  18012  fucidcl  18013  invfuc  18022  resssetc  18137  resscatc  18154  curf2cl  18276  yonedalem4c  18322  yonedalem3  18325  latdisdlem  18541  isrngd  20170  prdsrngd  20173  srgo2times  20209  srgcom4lem  20210  ringo2times  20272  ringcomlem  20276  isringd  20288  prdsringd  20318  isdomn4  20716  islmodd  20864  islmhm2  21037  rnglidl1  21242  rnglidlmsgrp  21256  rnglidlrng  21257  isphld  21672  ocvlss  21690  isassad  21885  mdetuni0  22627  mdetmul  22629  isngp4  24625  conway  27844  mulsprop  28156  tglowdim2ln  28659  f1otrgitv  28878  f1otrg  28879  f1otrge  28880  xmstrkgc  28900  eengtrkg  29001  eengtrkge  29002  submomnd  33087  ccfldsrarelvec  33721  weiunpo  36466  isrngod  37905  rngomndo  37942  isgrpda  37962  islfld  39063  lfladdcl  39072  lflnegcl  39076  lshpkrcl  39117  lclkr  41535  lclkrs  41541  lcfr  41587  copissgrp  48084  cznrng  48177  topdlat  48893  catprs2  48901  idmon  48908  idepi  48909  thincmon  49082  thincepi  49083  isthincd2  49086  oppcthinco  49088  oppcthinendcALT  49090  grptcmon  49190  grptcepi  49191