![]() |
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 1357 | . . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐶) → 𝜓) |
3 | 2 | ralrimiva 3140 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐶 𝜓) |
4 | 3 | ralrimiva 3140 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
5 | 4 | ralrimiva 3140 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1084 ∈ wcel 2098 ∀wral 3055 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 |
This theorem depends on definitions: df-bi 206 df-an 396 df-3an 1086 df-ral 3056 |
This theorem is referenced by: ispod 5590 swopolem 5591 isopolem 7338 caovassg 7602 caovcang 7605 caovordig 7609 caovordg 7611 caovdig 7618 caovdirg 7621 caofass 7704 caoftrn 7705 2oppccomf 17680 oppccomfpropd 17682 issubc3 17808 fthmon 17889 fuccocl 17929 fucidcl 17930 invfuc 17939 resssetc 18054 resscatc 18071 curf2cl 18196 yonedalem4c 18242 yonedalem3 18245 latdisdlem 18461 isrngd 20078 prdsrngd 20081 srgo2times 20117 srgcom4lem 20118 ringo2times 20174 ringcomlem 20178 isringd 20190 prdsringd 20220 islmodd 20712 islmhm2 20886 rnglidl1 21091 rnglidlmsgrp 21104 rnglidlrng 21105 isdomn4 21212 isphld 21547 ocvlss 21565 isassad 21759 mdetuni0 22478 mdetmul 22480 isngp4 24476 conway 27687 mulsprop 27985 tglowdim2ln 28410 f1otrgitv 28629 f1otrg 28630 f1otrge 28631 xmstrkgc 28651 eengtrkg 28752 eengtrkge 28753 submomnd 32734 ccfldsrarelvec 33264 isrngod 37279 rngomndo 37316 isgrpda 37336 islfld 38445 lfladdcl 38454 lflnegcl 38458 lshpkrcl 38499 lclkr 40917 lclkrs 40923 lcfr 40969 copissgrp 47123 cznrng 47216 topdlat 47908 catprs2 47911 idmon 47915 idepi 47916 thincmon 47933 thincepi 47934 isthincd2 47937 grptcmon 47995 grptcepi 47996 |
Copyright terms: Public domain | W3C validator |