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 1471 | . . . 4 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) | |
3 | 2 | 19.23h 1474 | . . 3 ⊢ (∀𝑥(𝜑 → ∃𝑥𝜑) ↔ (∃𝑥𝜑 → ∃𝑥𝜑)) |
4 | 1, 3 | mpbir 145 | . 2 ⊢ ∀𝑥(𝜑 → ∃𝑥𝜑) |
5 | 4 | spi 1516 | 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-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 19.8ad 1570 19.23bi 1571 exim 1578 19.43 1607 hbex 1615 19.2 1617 19.9t 1621 19.9h 1622 excomim 1641 19.38 1654 nexr 1670 sbequ1 1741 equs5e 1767 exdistrfor 1772 sbcof2 1782 mo2n 2027 euor2 2057 2moex 2085 2euex 2086 2moswapdc 2089 2exeu 2091 rspe 2481 rsp2e 2483 ceqex 2812 vn0m 3374 intab 3800 copsexg 4166 eusv2nf 4377 dmcosseq 4810 dminss 4953 imainss 4954 relssdmrn 5059 oprabid 5803 tfrlemibxssdm 6224 tfr1onlembxssdm 6240 tfrcllembxssdm 6253 snexxph 6838 nqprl 7359 nqpru 7360 ltsopr 7404 ltexprlemm 7408 recexprlemopl 7433 recexprlemopu 7435 suplocexprlemrl 7525 |
Copyright terms: Public domain | W3C validator |