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 1520 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → ∀𝑥∀𝑥(𝜑 → 𝜓)) | |
2 | hbe1 1471 | . 2 ⊢ (∃𝑥𝜓 → ∀𝑥∃𝑥𝜓) | |
3 | 19.8a 1569 | . . . 4 ⊢ (𝜓 → ∃𝑥𝜓) | |
4 | 3 | imim2i 12 | . . 3 ⊢ ((𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓)) |
5 | 4 | sps 1517 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓)) |
6 | 1, 2, 5 | exlimdh 1575 | 1 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1329 ∃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-ial 1514 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: eximi 1579 exbi 1583 eximdh 1590 19.29 1599 19.25 1605 alexim 1624 19.23t 1655 spimt 1714 equvini 1731 nfexd 1734 ax10oe 1769 sbcof2 1782 spsbim 1815 mor 2039 rexim 2524 elex22 2696 elex2 2697 vtoclegft 2753 spcimgft 2757 spcimegft 2759 spc2gv 2771 spc3gv 2773 ssoprab2 5820 bj-inf2vnlem1 13157 |
Copyright terms: Public domain | W3C validator |