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 1282 | . . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐶) → 𝜓) |
3 | 2 | ralrimiva 2949 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐶 𝜓) |
4 | 3 | ralrimiva 2949 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
5 | 4 | ralrimiva 2949 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 ∈ wcel 1977 ∀wral 2896 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 |
This theorem depends on definitions: df-bi 196 df-an 385 df-3an 1033 df-ral 2901 |
This theorem is referenced by: ispod 4967 swopolem 4968 isopolem 6495 caovassg 6730 caovcang 6733 caovordig 6737 caovordg 6739 caovdig 6746 caovdirg 6749 caofass 6829 caoftrn 6830 2oppccomf 16208 oppccomfpropd 16210 issubc3 16332 fthmon 16410 fuccocl 16447 fucidcl 16448 invfuc 16457 resssetc 16565 resscatc 16578 curf2cl 16694 yonedalem4c 16740 yonedalem3 16743 latdisdlem 17012 isringd 18408 prdsringd 18435 islmodd 18692 islmhm2 18859 isassad 19144 isphld 19818 ocvlss 19835 mdetuni0 20246 mdetmul 20248 isngp4 22226 tglowdim2ln 25346 f1otrgitv 25550 f1otrg 25551 f1otrge 25552 xmstrkgc 25566 eengtrkg 25665 eengtrkge 25666 submomnd 29041 isrngod 32867 rngomndo 32904 isgrpda 32924 islfld 33367 lfladdcl 33376 lflnegcl 33380 lshpkrcl 33421 lclkr 35840 lclkrs 35846 lcfr 35892 copissgrp 41598 lidlmsgrp 41716 lidlrng 41717 cznrng 41747 |
Copyright terms: Public domain | W3C validator |