Theorem ralrimivvva 2954

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1030   ∈ wcel 1976  ∀wral 2895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826

This theorem depends on definitions:  df-bi 195  df-an 384  df-3an 1032  df-ral 2900

This theorem is referenced by:  ispod  4957  swopolem  4958  isopolem  6473  caovassg  6707  caovcang  6710  caovordig  6714  caovordg  6716  caovdig  6723  caovdirg  6726  caofass  6806  caoftrn  6807  2oppccomf  16154  oppccomfpropd  16156  issubc3  16278  fthmon  16356  fuccocl  16393  fucidcl  16394  invfuc  16403  resssetc  16511  resscatc  16524  curf2cl  16640  yonedalem4c  16686  yonedalem3  16689  latdisdlem  16958  isringd  18354  prdsringd  18381  islmodd  18638  islmhm2  18805  isassad  19090  isphld  19763  ocvlss  19777  mdetuni0  20188  mdetmul  20190  isngp4  22166  tglowdim2ln  25264  f1otrgitv  25468  f1otrg  25469  f1otrge  25470  xmstrkgc  25484  eengtrkg  25583  eengtrkge  25584  submomnd  28847  isrngod  32670  rngomndo  32707  isgrpda  32727  islfld  33170  lfladdcl  33179  lflnegcl  33183  lshpkrcl  33224  lclkr  35643  lclkrs  35649  lcfr  35695  copissgrp  41600  lidlmsgrp  41718  lidlrng  41719  cznrng  41749