Theorem ralrimivvva 3178

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  ispod  5531  swopolem  5532  isopolem  7279  caovassg  7544  caovcang  7547  caovordig  7551  caovordg  7553  caovdig  7560  caovdirg  7563  caofass  7650  caoftrn  7651  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  20044  isrngd  20091  prdsrngd  20094  srgo2times  20130  srgcom4lem  20131  ringo2times  20193  ringcomlem  20197  isringd  20209  prdsringd  20239  isdomn4  20631  islmodd  20799  islmhm2  20972  rnglidl1  21169  rnglidlmsgrp  21183  rnglidlrng  21184  isphld  21591  ocvlss  21609  isassad  21802  mdetuni0  22536  mdetmul  22538  isngp4  24527  conway  27740  mulsprop  28069  tglowdim2ln  28629  f1otrgitv  28848  f1otrg  28849  f1otrge  28850  xmstrkgc  28864  eengtrkg  28964  eengtrkge  28965  ccfldsrarelvec  33684  weiunpo  36509  isrngod  37937  rngomndo  37974  isgrpda  37994  islfld  39160  lfladdcl  39169  lflnegcl  39173  lshpkrcl  39214  lclkr  41631  lclkrs  41637  lcfr  41683  copissgrp  48267  cznrng  48360  topdlat  49103  catprs2  49112  idmon  49120  idepi  49121  ssccatid  49172  resccatlem  49173  fthcomf  49257  thincmon  49533  thincepi  49534  isthincd2  49537  oppcthinco  49539  oppcthinendcALT  49541  grptcmon  49693  grptcepi  49694