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 1381	. . . 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 401   ∧ w3a 1103   ∈ wcel 2145  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ral 3079

This theorem is used by:  ispod  5576  swopolem  5577  isopolem  7349  caovassg  7615  caovcang  7618  caovordig  7622  caovordg  7624  caovdig  7631  caovdirg  7634  caofass  7721  caoftrn  7722  2oppccomf  17817  oppccomfpropd  17819  issubc3  17942  fthmon  18022  fuccocl  18060  fucidcl  18061  invfuc  18070  resssetc  18185  resscatc  18202  curf2cl  18323  yonedalem4c  18369  yonedalem3  18372  latdisdlem  18588  submomnd  20260  isrngd  20309  prdsrngd  20312  srgo2times  20352  srgcom4lem  20353  ringo2times  20417  ringcomlem  20421  isringd  20434  prdsringd  20462  isdomn4  20878  islmodd  21051  islmhm2  21223  rnglidl1  21422  rnglidlmsgrp  21444  rnglidlrng  21445  isphld  21868  ocvlss  21886  isassad  22081  mdetuni0  22844  mdetmul  22846  isngp4  24839  conway  28042  mulsprop  28393  tglowdim2ln  28997  f1otrgitv  29312  f1otrg  29313  f1otrge  29314  xmstrkgc  29328  eengtrkg  29429  eengtrkge  29430  ccfldsrarelvec  34168  weiunpo  37071  isrngod  38635  rngomndo  38672  isgrpda  38692  islfld  39922  lfladdcl  39931  lflnegcl  39935  lshpkrcl  39976  lclkr  42393  lclkrs  42399  lcfr  42445  copissgrp  49070  cznrng  49163  topdlat  49917  catprs2  49925  idmon  49933  idepi  49934  ssccatid  49985  resccatlem  49986  fthcomf  50070  thincmon  50346  thincepi  50347  isthincd2  50350  oppcthinco  50352  oppcthinendcALT  50354  grptcmon  50506  grptcepi  50507