![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > tru | GIF 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 1367 | . 2 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) | |
3 | 1, 2 | mpbir 146 | 1 ⊢ ⊤ |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1362 = wceq 1364 ⊤wtru 1365 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-tru 1367 |
This theorem is referenced by: fal 1371 dftru2 1372 mptru 1373 tbtru 1374 bitru 1376 trud 1380 truan 1381 truorfal 1417 falortru 1418 truimfal 1421 nftru 1477 euotd 4272 rabxfr 4488 reuhyp 4490 elabrex 5779 elabrexg 5780 caovcl 6052 caovass 6058 caovdi 6077 ectocl 6629 reef11 11742 bj-sbimeh 15002 bdtru 15062 bj-nn0suc0 15180 |
Copyright terms: Public domain | W3C validator |