![]() |
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 114 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) |
3 | 2 | rexlimiv 2517 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 1463 ∃wrex 2391 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1406 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-4 1470 ax-17 1489 ax-ial 1497 ax-i5r 1498 |
This theorem depends on definitions: df-bi 116 df-nf 1420 df-ral 2395 df-rex 2396 |
This theorem is referenced by: unon 4387 reg2exmidlema 4409 ssfilem 6722 diffitest 6734 fival 6810 elfi2 6812 fi0 6815 djuss 6907 updjud 6919 enumct 6952 finnum 6989 dmaddpqlem 7133 nqpi 7134 nq0nn 7198 recexprlemm 7380 rexanuz 10652 r19.2uz 10657 maxleast 10877 fsum2dlemstep 11095 fisumcom2 11099 0dvds 11361 even2n 11419 m1expe 11444 m1exp1 11446 epttop 12102 neipsm 12166 tgioo 12532 bj-nn0suc 12854 bj-nn0sucALT 12868 |
Copyright terms: Public domain | W3C validator |