![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rexlimdva | GIF version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.) |
Ref | Expression |
---|---|
rexlimdva.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
rexlimdva | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimdva.1 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) | |
2 | 1 | ex 108 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) |
3 | 2 | rexlimdv 2432 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ∈ wcel 1393 ∃wrex 2307 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 ax-i5r 1428 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-ral 2311 df-rex 2312 |
This theorem is referenced by: rexlimdvaa 2434 rexlimivv 2438 rexlimdvv 2439 ralxfrd 4194 rexxfrd 4195 fvelimab 5229 foco2 5318 elunirn 5405 f1elima 5412 tfrlem5 5930 tfrlemibacc 5940 tfrlemibfn 5942 nnaordex 6100 nnawordex 6101 ectocld 6172 phpm 6327 fin0 6342 fin0or 6343 ltexnqq 6506 ltbtwnnqq 6513 prarloclem4 6596 prarloc2 6602 genprndl 6619 genprndu 6620 prmuloc2 6665 1idprl 6688 1idpru 6689 cauappcvgprlemdisj 6749 cauappcvgprlemladdru 6754 cauappcvgprlemladdrl 6755 caucvgprlemladdrl 6776 recexgt0sr 6858 nntopi 6968 cnegexlem1 7186 cnegexlem2 7187 renegcl 7272 qmulz 8558 icc0r 8795 qbtwnzlemstep 9103 rebtwn2zlemstep 9107 frec2uzrand 9191 frecuzrdgfn 9198 shftlem 9417 caucvgre 9580 resqrexlemgt0 9618 climuni 9814 climshftlemg 9823 climcn1 9829 serif0 9871 |
Copyright terms: Public domain | W3C validator |