![]() |
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 1521 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → ∀𝑥∀𝑥(𝜑 → 𝜓)) | |
2 | hbe1 1472 | . 2 ⊢ (∃𝑥𝜓 → ∀𝑥∃𝑥𝜓) | |
3 | 19.8a 1570 | . . . 4 ⊢ (𝜓 → ∃𝑥𝜓) | |
4 | 3 | imim2i 12 | . . 3 ⊢ ((𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓)) |
5 | 4 | sps 1518 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓)) |
6 | 1, 2, 5 | exlimdh 1576 | 1 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1330 ∃wex 1469 |
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 1424 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-4 1488 ax-ial 1515 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: eximi 1580 exbi 1584 eximdh 1591 19.29 1600 19.25 1606 alexim 1625 19.23t 1656 spimt 1715 equvini 1732 nfexd 1735 ax10oe 1770 sbcof2 1783 spsbim 1816 mor 2042 rexim 2529 elex22 2704 elex2 2705 vtoclegft 2761 spcimgft 2765 spcimegft 2767 spc2gv 2780 spc3gv 2782 ssoprab2 5835 bj-inf2vnlem1 13339 |
Copyright terms: Public domain | W3C validator |