![]() |
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 3143 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐶 𝜓) |
4 | 3 | ralrimiva 3143 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
5 | 4 | ralrimiva 3143 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 ∈ wcel 2098 ∀wral 3058 |
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 395 df-3an 1086 df-ral 3059 |
This theorem is referenced by: ispod 5603 swopolem 5604 isopolem 7359 caovassg 7625 caovcang 7628 caovordig 7632 caovordg 7634 caovdig 7641 caovdirg 7644 caofass 7728 caoftrn 7729 2oppccomf 17714 oppccomfpropd 17716 issubc3 17842 fthmon 17923 fuccocl 17963 fucidcl 17964 invfuc 17973 resssetc 18088 resscatc 18105 curf2cl 18230 yonedalem4c 18276 yonedalem3 18279 latdisdlem 18495 isrngd 20120 prdsrngd 20123 srgo2times 20159 srgcom4lem 20160 ringo2times 20218 ringcomlem 20222 isringd 20234 prdsringd 20264 islmodd 20756 islmhm2 20930 rnglidl1 21135 rnglidlmsgrp 21148 rnglidlrng 21149 isdomn4 21257 isphld 21593 ocvlss 21611 isassad 21805 mdetuni0 22543 mdetmul 22545 isngp4 24541 conway 27752 mulsprop 28050 tglowdim2ln 28475 f1otrgitv 28694 f1otrg 28695 f1otrge 28696 xmstrkgc 28716 eengtrkg 28817 eengtrkge 28818 submomnd 32811 ccfldsrarelvec 33392 isrngod 37404 rngomndo 37441 isgrpda 37461 islfld 38566 lfladdcl 38575 lflnegcl 38579 lshpkrcl 38620 lclkr 41038 lclkrs 41044 lcfr 41090 copissgrp 47308 cznrng 47401 topdlat 48093 catprs2 48096 idmon 48100 idepi 48101 thincmon 48118 thincepi 48119 isthincd2 48122 grptcmon 48180 grptcepi 48181 |
Copyright terms: Public domain | W3C validator |