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 1506 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | alimdv.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | eximdh 1590 | 1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 2eximdv 1854 reximdv2 2531 cgsexg 2721 spc3egv 2777 euind 2871 ssel 3091 reupick 3360 reximdva0m 3378 uniss 3757 eusvnfb 4375 coss1 4694 coss2 4695 dmss 4738 dmcosseq 4810 funssres 5165 imain 5205 brprcneu 5414 fv3 5444 dffo4 5568 dffo5 5569 f1eqcocnv 5692 mapsn 6584 ctssdccl 6996 acfun 7063 ccfunen 7079 dmaddpq 7187 dmmulpq 7188 recexprlemlol 7434 recexprlemupu 7436 ioom 10038 ctinfom 11941 ctinf 11943 txcn 12444 |
Copyright terms: Public domain | W3C validator |