![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 19.8a | Unicode 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 1495 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | 19.23h 1498 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpbir 146 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | spi 1536 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
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 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 19.8ad 1591 19.23bi 1592 exim 1599 19.43 1628 hbex 1636 19.2 1638 19.9t 1642 19.9h 1643 excomim 1663 19.38 1676 nexr 1692 sbequ1 1768 equs5e 1795 exdistrfor 1800 sbcof2 1810 mo2n 2054 euor2 2084 2moex 2112 2euex 2113 2moswapdc 2116 2exeu 2118 rspe 2526 rsp2e 2528 ceqex 2864 vn0m 3434 intab 3871 copsexg 4241 eusv2nf 4453 dmcosseq 4894 dminss 5039 imainss 5040 relssdmrn 5145 oprabid 5901 tfrlemibxssdm 6322 tfr1onlembxssdm 6338 tfrcllembxssdm 6351 snexxph 6943 nqprl 7541 nqpru 7542 ltsopr 7586 ltexprlemm 7590 recexprlemopl 7615 recexprlemopu 7617 suplocexprlemrl 7707 |
Copyright terms: Public domain | W3C validator |