![]() |
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 1302 | . 2 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) | |
3 | 1, 2 | mpbir 145 | 1 ⊢ ⊤ |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1297 = wceq 1299 ⊤wtru 1300 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-tru 1302 |
This theorem is referenced by: fal 1306 dftru2 1307 mptru 1308 tbtru 1309 bitru 1311 a1tru 1315 truan 1316 truorfal 1352 falortru 1353 truimfal 1356 nftru 1410 euotd 4114 rabxfr 4329 reuhyp 4331 elabrex 5591 caovcl 5857 caovass 5863 caovdi 5882 ectocl 6426 reef11 11204 bj-sbimeh 12561 bdtru 12611 bj-nn0suc0 12733 |
Copyright terms: Public domain | W3C validator |