![]() |
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 1313 | . . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐶) → 𝜓) |
3 | 2 | ralrimiva 2995 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐶 𝜓) |
4 | 3 | ralrimiva 2995 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
5 | 4 | ralrimiva 2995 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1054 ∈ wcel 2030 ∀wral 2941 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 |
This theorem depends on definitions: df-bi 197 df-an 385 df-3an 1056 df-ral 2946 |
This theorem is referenced by: ispod 5072 swopolem 5073 isopolem 6635 caovassg 6874 caovcang 6877 caovordig 6881 caovordg 6883 caovdig 6890 caovdirg 6893 caofass 6973 caoftrn 6974 2oppccomf 16432 oppccomfpropd 16434 issubc3 16556 fthmon 16634 fuccocl 16671 fucidcl 16672 invfuc 16681 resssetc 16789 resscatc 16802 curf2cl 16918 yonedalem4c 16964 yonedalem3 16967 latdisdlem 17236 isringd 18631 prdsringd 18658 islmodd 18917 islmhm2 19086 isassad 19371 isphld 20047 ocvlss 20064 mdetuni0 20475 mdetmul 20477 isngp4 22463 tglowdim2ln 25591 f1otrgitv 25795 f1otrg 25796 f1otrge 25797 xmstrkgc 25811 eengtrkg 25910 eengtrkge 25911 submomnd 29838 conway 32035 isrngod 33827 rngomndo 33864 isgrpda 33884 islfld 34667 lfladdcl 34676 lflnegcl 34680 lshpkrcl 34721 lclkr 37139 lclkrs 37145 lcfr 37191 copissgrp 42133 lidlmsgrp 42251 lidlrng 42252 cznrng 42280 |
Copyright terms: Public domain | W3C validator |