![]() |
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 | ⊢ (φ → ∃xφ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . . 3 ⊢ (∃xφ → ∃xφ) | |
2 | hbe1 1381 | . . . 4 ⊢ (∃xφ → ∀x∃xφ) | |
3 | 2 | 19.23h 1384 | . . 3 ⊢ (∀x(φ → ∃xφ) ↔ (∃xφ → ∃xφ)) |
4 | 1, 3 | mpbir 134 | . 2 ⊢ ∀x(φ → ∃xφ) |
5 | 4 | spi 1426 | 1 ⊢ (φ → ∃xφ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1240 ∃wex 1378 |
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 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 19.23bi 1480 exim 1487 19.43 1516 hbex 1524 19.2 1526 19.9t 1530 19.9h 1531 excomim 1550 19.38 1563 nexr 1579 sbequ1 1648 equs5e 1673 exdistrfor 1678 sbcof2 1688 mo2n 1925 euor2 1955 2moex 1983 2euex 1984 2moswapdc 1987 2exeu 1989 rspe 2364 rsp2e 2366 ceqex 2665 vn0m 3226 intab 3635 copsexg 3972 eusv2nf 4154 dmcosseq 4546 dminss 4681 imainss 4682 relssdmrn 4784 oprabid 5480 tfrlemibxssdm 5882 nqprl 6533 ltsopr 6570 ltexprlemm 6574 recexprlemopl 6597 recexprlemopu 6599 |
Copyright terms: Public domain | W3C validator |