Theorem ralrimivvva 3184

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ral 3053

This theorem is referenced by:  ispod  5543  swopolem  5544  isopolem  7295  caovassg  7560  caovcang  7563  caovordig  7567  caovordg  7569  caovdig  7576  caovdirg  7579  caofass  7666  caoftrn  7667  2oppccomf  17686  oppccomfpropd  17688  issubc3  17811  fthmon  17891  fuccocl  17929  fucidcl  17930  invfuc  17939  resssetc  18054  resscatc  18071  curf2cl  18192  yonedalem4c  18238  yonedalem3  18241  latdisdlem  18457  submomnd  20102  isrngd  20149  prdsrngd  20152  srgo2times  20188  srgcom4lem  20189  ringo2times  20251  ringcomlem  20255  isringd  20267  prdsringd  20295  isdomn4  20688  islmodd  20856  islmhm2  21029  rnglidl1  21226  rnglidlmsgrp  21240  rnglidlrng  21241  isphld  21648  ocvlss  21666  isassad  21859  mdetuni0  22600  mdetmul  22602  isngp4  24591  conway  27789  mulsprop  28140  tglowdim2ln  28737  f1otrgitv  28956  f1otrg  28957  f1otrge  28958  xmstrkgc  28972  eengtrkg  29073  eengtrkge  29074  ccfldsrarelvec  33835  weiunpo  36667  isrngod  38239  rngomndo  38276  isgrpda  38296  islfld  39528  lfladdcl  39537  lflnegcl  39541  lshpkrcl  39582  lclkr  41999  lclkrs  42005  lcfr  42051  copissgrp  48662  cznrng  48755  topdlat  49497  catprs2  49505  idmon  49513  idepi  49514  ssccatid  49565  resccatlem  49566  fthcomf  49650  thincmon  49926  thincepi  49927  isthincd2  49930  oppcthinco  49932  oppcthinendcALT  49934  grptcmon  50086  grptcepi  50087