Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ralrimivvva | Structured version Visualization version GIF version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with triple quantification.) (Contributed by Mario Carneiro, 9-Jul-2014.) |
Ref | Expression |
---|---|
ralrimivvva.1 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) → 𝜓) |
Ref | Expression |
---|---|
ralrimivvva | ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralrimivvva.1 | . . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) → 𝜓) | |
2 | 1 | 3anassrs 1356 | . . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐶) → 𝜓) |
3 | 2 | ralrimiva 3184 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐶 𝜓) |
4 | 3 | ralrimiva 3184 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
5 | 4 | ralrimiva 3184 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 ∈ wcel 2114 ∀wral 3140 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 |
This theorem depends on definitions: df-bi 209 df-an 399 df-3an 1085 df-ral 3145 |
This theorem is referenced by: ispod 5484 swopolem 5485 isopolem 7100 caovassg 7348 caovcang 7351 caovordig 7355 caovordg 7357 caovdig 7364 caovdirg 7367 caofass 7445 caoftrn 7446 2oppccomf 16997 oppccomfpropd 16999 issubc3 17121 fthmon 17199 fuccocl 17236 fucidcl 17237 invfuc 17246 resssetc 17354 resscatc 17367 curf2cl 17483 yonedalem4c 17529 yonedalem3 17532 latdisdlem 17801 isringd 19337 prdsringd 19364 islmodd 19642 islmhm2 19812 isassad 20098 isphld 20800 ocvlss 20818 mdetuni0 21232 mdetmul 21234 isngp4 23223 tglowdim2ln 26439 f1otrgitv 26658 f1otrg 26659 f1otrge 26660 xmstrkgc 26674 eengtrkg 26774 eengtrkge 26775 submomnd 30713 ccfldsrarelvec 31058 conway 33266 isrngod 35178 rngomndo 35215 isgrpda 35235 islfld 36200 lfladdcl 36209 lflnegcl 36213 lshpkrcl 36254 lclkr 38671 lclkrs 38677 lcfr 38723 copissgrp 44082 lidlmsgrp 44204 lidlrng 44205 cznrng 44233 |
Copyright terms: Public domain | W3C validator |