![]() |
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 1526 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | alimdv.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | eximdh 1611 | 1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1492 |
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 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 2eximdv 1882 reximdv2 2576 cgsexg 2772 spc3egv 2829 euind 2924 ssel 3149 reupick 3419 reximdva0m 3438 uniss 3830 eusvnfb 4454 coss1 4782 coss2 4783 dmss 4826 dmcosseq 4898 funssres 5258 imain 5298 brprcneu 5508 fv3 5538 dffo4 5664 dffo5 5665 f1eqcocnv 5791 mapsn 6689 ctssdccl 7109 acfun 7205 ccfunen 7262 cc4f 7267 cc4n 7269 dmaddpq 7377 dmmulpq 7378 recexprlemlol 7624 recexprlemupu 7626 ioom 10258 ctinfom 12423 ctinf 12425 omctfn 12438 nninfdclemp1 12445 subgintm 13011 txcn 13668 |
Copyright terms: Public domain | W3C validator |