Theorem ralrimivvva 3211

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ral 3068

This theorem is referenced by:  ispod  5617  swopolem  5618  isopolem  7381  caovassg  7648  caovcang  7651  caovordig  7655  caovordg  7657  caovdig  7664  caovdirg  7667  caofass  7752  caoftrn  7753  2oppccomf  17785  oppccomfpropd  17787  issubc3  17913  fthmon  17994  fuccocl  18034  fucidcl  18035  invfuc  18044  resssetc  18159  resscatc  18176  curf2cl  18301  yonedalem4c  18347  yonedalem3  18350  latdisdlem  18566  isrngd  20200  prdsrngd  20203  srgo2times  20239  srgcom4lem  20240  ringo2times  20298  ringcomlem  20302  isringd  20314  prdsringd  20344  isdomn4  20738  islmodd  20886  islmhm2  21060  rnglidl1  21265  rnglidlmsgrp  21279  rnglidlrng  21280  isphld  21695  ocvlss  21713  isassad  21908  mdetuni0  22648  mdetmul  22650  isngp4  24646  conway  27862  mulsprop  28174  tglowdim2ln  28677  f1otrgitv  28896  f1otrg  28897  f1otrge  28898  xmstrkgc  28918  eengtrkg  29019  eengtrkge  29020  submomnd  33060  ccfldsrarelvec  33681  weiunpo  36431  isrngod  37858  rngomndo  37895  isgrpda  37915  islfld  39018  lfladdcl  39027  lflnegcl  39031  lshpkrcl  39072  lclkr  41490  lclkrs  41496  lcfr  41542  copissgrp  47891  cznrng  47984  topdlat  48676  catprs2  48679  idmon  48683  idepi  48684  thincmon  48701  thincepi  48702  isthincd2  48705  grptcmon  48763  grptcepi  48764