Theorem ralrimivvva 3217

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-ral 3086

This theorem is referenced by:  ispod  5579  swopolem  5580  isopolem  7344  caovassg  7609  caovcang  7612  caovordig  7616  caovordg  7618  caovdig  7625  caovdirg  7628  caofass  7715  caoftrn  7716  2oppccomf  17781  oppccomfpropd  17783  issubc3  17906  fthmon  17986  fuccocl  18024  fucidcl  18025  invfuc  18034  resssetc  18149  resscatc  18166  curf2cl  18287  yonedalem4c  18333  yonedalem3  18336  latdisdlem  18552  submomnd  20202  isrngd  20251  prdsrngd  20254  srgo2times  20294  srgcom4lem  20295  ringo2times  20358  ringcomlem  20362  isringd  20374  prdsringd  20402  isdomn4  20800  islmodd  20965  islmhm2  21137  rnglidl1  21336  rnglidlmsgrp  21354  rnglidlrng  21355  isphld  21773  ocvlss  21791  isassad  21984  mdetuni0  22747  mdetmul  22749  isngp4  24738  conway  27938  mulsprop  28289  tglowdim2ln  28887  f1otrgitv  29160  f1otrg  29161  f1otrge  29162  xmstrkgc  29176  eengtrkg  29277  eengtrkge  29278  ccfldsrarelvec  34006  weiunpo  36899  isrngod  38472  rngomndo  38509  isgrpda  38529  islfld  39761  lfladdcl  39770  lflnegcl  39774  lshpkrcl  39815  lclkr  42232  lclkrs  42238  lcfr  42284  copissgrp  48857  cznrng  48950  topdlat  49702  catprs2  49710  idmon  49718  idepi  49719  ssccatid  49770  resccatlem  49771  fthcomf  49855  thincmon  50131  thincepi  50132  isthincd2  50135  oppcthinco  50137  oppcthinendcALT  50139  grptcmon  50291  grptcepi  50292