| 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 1549 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
| 2 | alimdv.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 3 | 1, 2 | eximdh 1634 | 1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∃wex 1515 |
| 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 1470 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-4 1533 ax-17 1549 ax-ial 1557 |
| This theorem depends on definitions: df-bi 117 |
| This theorem is referenced by: 2eximdv 1905 reximdv2 2605 cgsexg 2807 spc3egv 2865 euind 2960 ssel 3187 reupick 3457 reximdva0m 3476 uniss 3871 eusvnfb 4501 coss1 4833 coss2 4834 dmss 4877 dmcosseq 4950 funssres 5313 imain 5356 brprcneu 5569 fv3 5599 dffo4 5728 dffo5 5729 f1eqcocnv 5860 mapsn 6777 ctssdccl 7213 acfun 7319 ccfunen 7376 cc4f 7381 cc4n 7383 dmaddpq 7492 dmmulpq 7493 recexprlemlol 7739 recexprlemupu 7741 ioom 10403 ctinfom 12799 ctinf 12801 omctfn 12814 nninfdclemp1 12821 ptex 13096 subgintm 13534 txcn 14747 |
| Copyright terms: Public domain | W3C validator |