![]() |
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 1340 | . . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐶) → 𝜓) |
3 | 2 | ralrimiva 3126 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐶 𝜓) |
4 | 3 | ralrimiva 3126 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
5 | 4 | ralrimiva 3126 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∧ w3a 1068 ∈ wcel 2050 ∀wral 3082 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 |
This theorem depends on definitions: df-bi 199 df-an 388 df-3an 1070 df-ral 3087 |
This theorem is referenced by: ispod 5328 swopolem 5329 isopolem 6915 caovassg 7156 caovcang 7159 caovordig 7163 caovordg 7165 caovdig 7172 caovdirg 7175 caofass 7255 caoftrn 7256 2oppccomf 16847 oppccomfpropd 16849 issubc3 16971 fthmon 17049 fuccocl 17086 fucidcl 17087 invfuc 17096 resssetc 17204 resscatc 17217 curf2cl 17333 yonedalem4c 17379 yonedalem3 17382 latdisdlem 17651 isringd 19052 prdsringd 19079 islmodd 19356 islmhm2 19526 isassad 19811 isphld 20494 ocvlss 20512 mdetuni0 20928 mdetmul 20930 isngp4 22918 tglowdim2ln 26133 f1otrgitv 26353 f1otrg 26354 f1otrge 26355 xmstrkgc 26369 eengtrkg 26469 eengtrkge 26470 submomnd 30429 ccfldsrarelvec 30685 conway 32785 isrngod 34618 rngomndo 34655 isgrpda 34675 islfld 35643 lfladdcl 35652 lflnegcl 35656 lshpkrcl 35697 lclkr 38114 lclkrs 38120 lcfr 38166 copissgrp 43443 lidlmsgrp 43561 lidlrng 43562 cznrng 43590 |
Copyright terms: Public domain | W3C validator |