Theorem ralrimivvva 3001

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054   ∈ wcel 2030  ∀wral 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879

This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1056  df-ral 2946

This theorem is referenced by:  ispod  5072  swopolem  5073  isopolem  6635  caovassg  6874  caovcang  6877  caovordig  6881  caovordg  6883  caovdig  6890  caovdirg  6893  caofass  6973  caoftrn  6974  2oppccomf  16432  oppccomfpropd  16434  issubc3  16556  fthmon  16634  fuccocl  16671  fucidcl  16672  invfuc  16681  resssetc  16789  resscatc  16802  curf2cl  16918  yonedalem4c  16964  yonedalem3  16967  latdisdlem  17236  isringd  18631  prdsringd  18658  islmodd  18917  islmhm2  19086  isassad  19371  isphld  20047  ocvlss  20064  mdetuni0  20475  mdetmul  20477  isngp4  22463  tglowdim2ln  25591  f1otrgitv  25795  f1otrg  25796  f1otrge  25797  xmstrkgc  25811  eengtrkg  25910  eengtrkge  25911  submomnd  29838  conway  32035  isrngod  33827  rngomndo  33864  isgrpda  33884  islfld  34667  lfladdcl  34676  lflnegcl  34680  lshpkrcl  34721  lclkr  37139  lclkrs  37145  lcfr  37191  copissgrp  42133  lidlmsgrp  42251  lidlrng  42252  cznrng  42280