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 1290 | . . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐶) → 𝜓) |
3 | 2 | ralrimiva 2966 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐶 𝜓) |
4 | 3 | ralrimiva 2966 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
5 | 4 | ralrimiva 2966 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 ∈ wcel 1990 ∀wral 2912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 |
This theorem depends on definitions: df-bi 197 df-an 386 df-3an 1039 df-ral 2917 |
This theorem is referenced by: ispod 5043 swopolem 5044 isopolem 6595 caovassg 6832 caovcang 6835 caovordig 6839 caovordg 6841 caovdig 6848 caovdirg 6851 caofass 6931 caoftrn 6932 2oppccomf 16385 oppccomfpropd 16387 issubc3 16509 fthmon 16587 fuccocl 16624 fucidcl 16625 invfuc 16634 resssetc 16742 resscatc 16755 curf2cl 16871 yonedalem4c 16917 yonedalem3 16920 latdisdlem 17189 isringd 18585 prdsringd 18612 islmodd 18869 islmhm2 19038 isassad 19323 isphld 19999 ocvlss 20016 mdetuni0 20427 mdetmul 20429 isngp4 22416 tglowdim2ln 25546 f1otrgitv 25750 f1otrg 25751 f1otrge 25752 xmstrkgc 25766 eengtrkg 25865 eengtrkge 25866 submomnd 29710 conway 31910 isrngod 33697 rngomndo 33734 isgrpda 33754 islfld 34349 lfladdcl 34358 lflnegcl 34362 lshpkrcl 34403 lclkr 36822 lclkrs 36828 lcfr 36874 copissgrp 41808 lidlmsgrp 41926 lidlrng 41927 cznrng 41955 |
Copyright terms: Public domain | W3C validator |