![]() |
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 1454 | . . . 4 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) | |
3 | 2 | 19.23h 1457 | . . 3 ⊢ (∀𝑥(𝜑 → ∃𝑥𝜑) ↔ (∃𝑥𝜑 → ∃𝑥𝜑)) |
4 | 1, 3 | mpbir 145 | . 2 ⊢ ∀𝑥(𝜑 → ∃𝑥𝜑) |
5 | 4 | spi 1499 | 1 ⊢ (𝜑 → ∃𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1312 ∃wex 1451 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-4 1470 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 19.8ad 1553 19.23bi 1554 exim 1561 19.43 1590 hbex 1598 19.2 1600 19.9t 1604 19.9h 1605 excomim 1624 19.38 1637 nexr 1653 sbequ1 1724 equs5e 1749 exdistrfor 1754 sbcof2 1764 mo2n 2003 euor2 2033 2moex 2061 2euex 2062 2moswapdc 2065 2exeu 2067 rspe 2455 rsp2e 2457 ceqex 2782 vn0m 3340 intab 3766 copsexg 4126 eusv2nf 4337 dmcosseq 4768 dminss 4911 imainss 4912 relssdmrn 5017 oprabid 5757 tfrlemibxssdm 6178 tfr1onlembxssdm 6194 tfrcllembxssdm 6207 snexxph 6790 nqprl 7307 nqpru 7308 ltsopr 7352 ltexprlemm 7356 recexprlemopl 7381 recexprlemopu 7383 |
Copyright terms: Public domain | W3C validator |