Theorem ralrimivvva 3183

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  ispod  5542  swopolem  5543  isopolem  7293  caovassg  7558  caovcang  7561  caovordig  7565  caovordg  7567  caovdig  7574  caovdirg  7577  caofass  7664  caoftrn  7665  2oppccomf  17652  oppccomfpropd  17654  issubc3  17777  fthmon  17857  fuccocl  17895  fucidcl  17896  invfuc  17905  resssetc  18020  resscatc  18037  curf2cl  18158  yonedalem4c  18204  yonedalem3  18207  latdisdlem  18423  submomnd  20065  isrngd  20112  prdsrngd  20115  srgo2times  20151  srgcom4lem  20152  ringo2times  20214  ringcomlem  20218  isringd  20230  prdsringd  20260  isdomn4  20653  islmodd  20821  islmhm2  20994  rnglidl1  21191  rnglidlmsgrp  21205  rnglidlrng  21206  isphld  21613  ocvlss  21631  isassad  21824  mdetuni0  22569  mdetmul  22571  isngp4  24560  conway  27779  mulsprop  28130  tglowdim2ln  28727  f1otrgitv  28946  f1otrg  28947  f1otrge  28948  xmstrkgc  28962  eengtrkg  29063  eengtrkge  29064  ccfldsrarelvec  33830  weiunpo  36661  isrngod  38101  rngomndo  38138  isgrpda  38158  islfld  39390  lfladdcl  39399  lflnegcl  39403  lshpkrcl  39444  lclkr  41861  lclkrs  41867  lcfr  41913  copissgrp  48481  cznrng  48574  topdlat  49316  catprs2  49324  idmon  49332  idepi  49333  ssccatid  49384  resccatlem  49385  fthcomf  49469  thincmon  49745  thincepi  49746  isthincd2  49749  oppcthinco  49751  oppcthinendcALT  49753  grptcmon  49905  grptcepi  49906