Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > tru | Unicode version |
Description: The truth value is provable. (Contributed by Anthony Hart, 13-Oct-2010.) |
Ref | Expression |
---|---|
tru |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 | |
2 | df-tru 1246 | . 2 | |
3 | 1, 2 | mpbir 134 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1241 wceq 1243 wtru 1244 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 df-tru 1246 |
This theorem is referenced by: fal 1250 dftru2 1251 trud 1252 tbtru 1253 bitru 1255 a1tru 1259 truan 1260 truorfal 1297 falortru 1298 truimfal 1301 nftru 1355 euotd 3991 rabxfr 4202 reuhyp 4204 elabrex 5397 caovcl 5655 caovass 5661 caovdi 5680 ectocl 6173 bj-sbimeh 9912 bdtru 9952 bj-nn0suc0 10075 |
Copyright terms: Public domain | W3C validator |