![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ralrimivvva | 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 1231 | . . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐶) → 𝜓) |
3 | 2 | ralrimiva 2563 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐶 𝜓) |
4 | 3 | ralrimiva 2563 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
5 | 4 | ralrimiva 2563 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 980 ∈ wcel 2160 ∀wral 2468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-4 1521 ax-17 1537 |
This theorem depends on definitions: df-bi 117 df-3an 982 df-nf 1472 df-ral 2473 |
This theorem is referenced by: ispod 4322 swopolem 4323 ordwe 4593 wessep 4595 isopolem 5844 caovassg 6056 caovcang 6059 caovordig 6063 caovordg 6065 caovdig 6072 caovdirg 6075 caoftrn 6133 netap 7284 2omotaplemap 7287 isrngd 13324 isringd 13412 aprap 13619 islmodd 13626 rnglidlmsgrp 13830 rnglidlrng 13831 |
Copyright terms: Public domain | W3C validator |