Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > exim | GIF version |
Description: Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
Ref | Expression |
---|---|
exim | ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hba1 1433 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → ∀𝑥∀𝑥(𝜑 → 𝜓)) | |
2 | hbe1 1384 | . 2 ⊢ (∃𝑥𝜓 → ∀𝑥∃𝑥𝜓) | |
3 | 19.8a 1482 | . . . 4 ⊢ (𝜓 → ∃𝑥𝜓) | |
4 | 3 | imim2i 12 | . . 3 ⊢ ((𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓)) |
5 | 4 | sps 1430 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓)) |
6 | 1, 2, 5 | exlimdh 1487 | 1 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1241 ∃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-ial 1427 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: eximi 1491 exbi 1495 eximdh 1502 19.29 1511 19.25 1517 alexim 1536 19.23t 1567 spimt 1624 equvini 1641 nfexd 1644 ax10oe 1678 sbcof2 1691 spsbim 1724 mor 1942 rexim 2413 elex22 2569 elex2 2570 vtoclegft 2625 spcimgft 2629 spcimegft 2631 spc2gv 2643 spc3gv 2645 ssoprab2 5561 bj-inf2vnlem1 10095 |
Copyright terms: Public domain | W3C validator |