![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rexlimiva | GIF version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.) |
Ref | Expression |
---|---|
rexlimiva.1 | ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) |
Ref | Expression |
---|---|
rexlimiva | ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimiva.1 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) | |
2 | 1 | ex 115 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) |
3 | 2 | rexlimiv 2588 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∈ wcel 2148 ∃wrex 2456 |
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 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 ax-i5r 1535 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-ral 2460 df-rex 2461 |
This theorem is referenced by: unon 4512 reg2exmidlema 4535 ssfilem 6877 diffitest 6889 fival 6971 elfi2 6973 fi0 6976 djuss 7071 updjud 7083 enumct 7116 finnum 7184 dmaddpqlem 7378 nqpi 7379 nq0nn 7443 recexprlemm 7625 rexanuz 10999 r19.2uz 11004 maxleast 11224 fsum2dlemstep 11444 fisumcom2 11448 fprod2dlemstep 11632 fprodcom2fi 11636 0dvds 11820 even2n 11881 m1expe 11906 m1exp1 11908 modprm0 12256 dfgrp2 12907 epttop 13675 neipsm 13739 tgioo 14131 sin0pilem2 14288 pilem3 14289 bj-nn0suc 14801 bj-nn0sucALT 14815 trirec0xor 14878 |
Copyright terms: Public domain | W3C validator |