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 1319 | . 2 | |
3 | 1, 2 | mpbir 145 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1314 wceq 1316 wtru 1317 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-tru 1319 |
This theorem is referenced by: fal 1323 dftru2 1324 mptru 1325 tbtru 1326 bitru 1328 a1tru 1332 truan 1333 truorfal 1369 falortru 1370 truimfal 1373 nftru 1427 euotd 4146 rabxfr 4361 reuhyp 4363 elabrex 5627 caovcl 5893 caovass 5899 caovdi 5918 ectocl 6464 reef11 11333 bj-sbimeh 12906 bdtru 12957 bj-nn0suc0 13075 |
Copyright terms: Public domain | W3C validator |