![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 19.8a | GIF version |
Description: If a wff is true, then it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
19.8a | ⊢ (𝜑 → ∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . . 3 ⊢ (∃𝑥𝜑 → ∃𝑥𝜑) | |
2 | hbe1 1506 | . . . 4 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) | |
3 | 2 | 19.23h 1509 | . . 3 ⊢ (∀𝑥(𝜑 → ∃𝑥𝜑) ↔ (∃𝑥𝜑 → ∃𝑥𝜑)) |
4 | 1, 3 | mpbir 146 | . 2 ⊢ ∀𝑥(𝜑 → ∃𝑥𝜑) |
5 | 4 | spi 1547 | 1 ⊢ (𝜑 → ∃𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1362 ∃wex 1503 |
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-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-4 1521 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 19.8ad 1602 19.23bi 1603 exim 1610 19.43 1639 hbex 1647 19.2 1649 19.9t 1653 19.9h 1654 excomim 1674 19.38 1687 nexr 1703 sbequ1 1779 equs5e 1806 exdistrfor 1811 sbcof2 1821 mo2n 2066 euor2 2096 2moex 2124 2euex 2125 2moswapdc 2128 2exeu 2130 rspe 2539 rsp2e 2541 ceqex 2879 vn0m 3449 intab 3891 copsexg 4265 eusv2nf 4477 dmcosseq 4919 dminss 5064 imainss 5065 relssdmrn 5170 oprabid 5932 tfrlemibxssdm 6356 tfr1onlembxssdm 6372 tfrcllembxssdm 6385 snexxph 6983 nqprl 7585 nqpru 7586 ltsopr 7630 ltexprlemm 7634 recexprlemopl 7659 recexprlemopu 7661 suplocexprlemrl 7751 |
Copyright terms: Public domain | W3C validator |