Theorem ralrimivvva 3210

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102   ∈ wcel 2142  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104  df-ral 3079

This theorem is used by:  ispod  5577  swopolem  5578  isopolem  7343  caovassg  7610  caovcang  7613  caovordig  7617  caovordg  7619  caovdig  7626  caovdirg  7629  caofass  7716  caoftrn  7717  2oppccomf  17787  oppccomfpropd  17789  issubc3  17912  fthmon  17992  fuccocl  18030  fucidcl  18031  invfuc  18040  resssetc  18155  resscatc  18172  curf2cl  18293  yonedalem4c  18339  yonedalem3  18342  latdisdlem  18558  submomnd  20208  isrngd  20257  prdsrngd  20260  srgo2times  20300  srgcom4lem  20301  ringo2times  20365  ringcomlem  20369  isringd  20381  prdsringd  20409  isdomn4  20825  islmodd  20998  islmhm2  21170  rnglidl1  21369  rnglidlmsgrp  21391  rnglidlrng  21392  isphld  21815  ocvlss  21833  isassad  22026  mdetuni0  22789  mdetmul  22791  isngp4  24780  conway  27983  mulsprop  28334  tglowdim2ln  28936  f1otrgitv  29230  f1otrg  29231  f1otrge  29232  xmstrkgc  29246  eengtrkg  29347  eengtrkge  29348  ccfldsrarelvec  34070  weiunpo  37004  isrngod  38577  rngomndo  38614  isgrpda  38634  islfld  39864  lfladdcl  39873  lflnegcl  39877  lshpkrcl  39918  lclkr  42335  lclkrs  42341  lcfr  42387  copissgrp  48961  cznrng  49054  topdlat  49810  catprs2  49818  idmon  49826  idepi  49827  ssccatid  49878  resccatlem  49879  fthcomf  49963  thincmon  50239  thincepi  50240  isthincd2  50243  oppcthinco  50245  oppcthinendcALT  50247  grptcmon  50399  grptcepi  50400