| 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 1361 | . . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐶) → 𝜓) |
| 3 | 2 | ralrimiva 3146 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐶 𝜓) |
| 4 | 3 | ralrimiva 3146 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
| 5 | 4 | ralrimiva 3146 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 ∈ wcel 2108 ∀wral 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-ral 3062 |
| This theorem is referenced by: ispod 5601 swopolem 5602 isopolem 7365 caovassg 7631 caovcang 7634 caovordig 7638 caovordg 7640 caovdig 7647 caovdirg 7650 caofass 7737 caoftrn 7738 2oppccomf 17768 oppccomfpropd 17770 issubc3 17894 fthmon 17974 fuccocl 18012 fucidcl 18013 invfuc 18022 resssetc 18137 resscatc 18154 curf2cl 18276 yonedalem4c 18322 yonedalem3 18325 latdisdlem 18541 isrngd 20170 prdsrngd 20173 srgo2times 20209 srgcom4lem 20210 ringo2times 20272 ringcomlem 20276 isringd 20288 prdsringd 20318 isdomn4 20716 islmodd 20864 islmhm2 21037 rnglidl1 21242 rnglidlmsgrp 21256 rnglidlrng 21257 isphld 21672 ocvlss 21690 isassad 21885 mdetuni0 22627 mdetmul 22629 isngp4 24625 conway 27844 mulsprop 28156 tglowdim2ln 28659 f1otrgitv 28878 f1otrg 28879 f1otrge 28880 xmstrkgc 28900 eengtrkg 29001 eengtrkge 29002 submomnd 33087 ccfldsrarelvec 33721 weiunpo 36466 isrngod 37905 rngomndo 37942 isgrpda 37962 islfld 39063 lfladdcl 39072 lflnegcl 39076 lshpkrcl 39117 lclkr 41535 lclkrs 41541 lcfr 41587 copissgrp 48084 cznrng 48177 topdlat 48893 catprs2 48901 idmon 48908 idepi 48909 thincmon 49082 thincepi 49083 isthincd2 49086 oppcthinco 49088 oppcthinendcALT 49090 grptcmon 49190 grptcepi 49191 |
| Copyright terms: Public domain | W3C validator |