Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eximdv | GIF version |
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.) |
Ref | Expression |
---|---|
alimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
eximdv | ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1419 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | alimdv.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | eximdh 1502 | 1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1381 |
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 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 2eximdv 1762 reximdv2 2418 cgsexg 2589 spc3egv 2644 euind 2728 ssel 2939 reupick 3221 reximdva0m 3236 uniss 3601 eusvnfb 4186 coss1 4491 coss2 4492 dmss 4534 dmcosseq 4603 funssres 4942 imain 4981 brprcneu 5171 fv3 5197 dffo4 5315 dffo5 5316 f1eqcocnv 5431 dmaddpq 6477 dmmulpq 6478 recexprlemlol 6724 recexprlemupu 6726 |
Copyright terms: Public domain | W3C validator |