Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 19.8a | GIF version |
Description: If a wff is true, 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 1384 | . . . 4 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) | |
3 | 2 | 19.23h 1387 | . . 3 ⊢ (∀𝑥(𝜑 → ∃𝑥𝜑) ↔ (∃𝑥𝜑 → ∃𝑥𝜑)) |
4 | 1, 3 | mpbir 134 | . 2 ⊢ ∀𝑥(𝜑 → ∃𝑥𝜑) |
5 | 4 | spi 1429 | 1 ⊢ (𝜑 → ∃𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1241 ∃wex 1381 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 19.23bi 1483 exim 1490 19.43 1519 hbex 1527 19.2 1529 19.9t 1533 19.9h 1534 excomim 1553 19.38 1566 nexr 1582 sbequ1 1651 equs5e 1676 exdistrfor 1681 sbcof2 1691 mo2n 1928 euor2 1958 2moex 1986 2euex 1987 2moswapdc 1990 2exeu 1992 rspe 2370 rsp2e 2372 ceqex 2671 vn0m 3232 intab 3644 copsexg 3981 eusv2nf 4188 dmcosseq 4603 dminss 4738 imainss 4739 relssdmrn 4841 oprabid 5537 tfrlemibxssdm 5941 nqprl 6649 nqpru 6650 ltsopr 6694 ltexprlemm 6698 recexprlemopl 6723 recexprlemopu 6725 |
Copyright terms: Public domain | W3C validator |