Theorem ralrimivvva 3115

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087  df-ral 3068

This theorem is referenced by:  ispod  5503  swopolem  5504  isopolem  7196  caovassg  7448  caovcang  7451  caovordig  7455  caovordg  7457  caovdig  7464  caovdirg  7467  caofass  7548  caoftrn  7549  2oppccomf  17353  oppccomfpropd  17355  issubc3  17480  fthmon  17559  fuccocl  17598  fucidcl  17599  invfuc  17608  resssetc  17723  resscatc  17740  curf2cl  17865  yonedalem4c  17911  yonedalem3  17914  latdisdlem  18129  isringd  19739  prdsringd  19766  islmodd  20044  islmhm2  20215  isphld  20771  ocvlss  20789  isassad  20981  mdetuni0  21678  mdetmul  21680  isngp4  23674  tglowdim2ln  26916  f1otrgitv  27135  f1otrg  27136  f1otrge  27137  xmstrkgc  27156  eengtrkg  27257  eengtrkge  27258  submomnd  31238  ccfldsrarelvec  31643  conway  33920  isrngod  35983  rngomndo  36020  isgrpda  36040  islfld  37003  lfladdcl  37012  lflnegcl  37016  lshpkrcl  37057  lclkr  39474  lclkrs  39480  lcfr  39526  isdomn4  40100  copissgrp  45250  lidlmsgrp  45372  lidlrng  45373  cznrng  45401  topdlat  46178  catprs2  46181  idmon  46185  idepi  46186  thincmon  46203  thincepi  46204  isthincd2  46207  grptcmon  46263  grptcepi  46264