Theorem ralrimivvva 3208

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ral 3077

This theorem is used by:  ispod  5567  swopolem  5568  isopolem  7353  caovassg  7619  caovcang  7622  caovordig  7626  caovordg  7628  caovdig  7635  caovdirg  7638  caofass  7733  caoftrn  7734  2oppccomf  17899  oppccomfpropd  17901  issubc3  18024  fthmon  18104  fuccocl  18142  fucidcl  18143  invfuc  18152  resssetc  18267  resscatc  18284  curf2cl  18405  yonedalem4c  18451  yonedalem3  18454  latdisdlem  18670  submomnd  20346  isrngd  20395  prdsrngd  20398  srgo2times  20438  srgcom4lem  20439  ringo2times  20504  ringcomlem  20508  isringd  20522  prdsringd  20550  isdomn4  20967  islmodd  21141  islmhm2  21313  rnglidl1  21512  rnglidlmsgrp  21534  rnglidlrng  21535  isphld  21960  ocvlss  21978  isassad  22173  mdetuni0  22936  mdetmul  22938  isngp4  24931  conway  28165  mulsprop  28516  tglowdim2ln  29120  f1otrgitv  29447  f1otrg  29448  f1otrge  29449  xmstrkgc  29463  eengtrkg  29564  eengtrkge  29565  ccfldsrarelvec  34303  weiunpo  37253  isrngod  38833  rngomndo  38870  isgrpda  38890  islfld  40120  lfladdcl  40129  lflnegcl  40133  lshpkrcl  40174  lclkr  42591  lclkrs  42597  lcfr  42643  copissgrp  49265  cznrng  49358  topdlat  50112  catprs2  50120  idmon  50128  idepi  50129  ssccatid  50180  resccatlem  50181  fthcomf  50265  thincmon  50541  thincepi  50542  isthincd2  50545  oppcthinco  50547  oppcthinendcALT  50549  grptcmon  50701  grptcepi  50702