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 1334 | . 2 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) | |
3 | 1, 2 | mpbir 145 | 1 ⊢ ⊤ |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1329 = wceq 1331 ⊤wtru 1332 |
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 1334 |
This theorem is referenced by: fal 1338 dftru2 1339 mptru 1340 tbtru 1341 bitru 1343 a1tru 1347 truan 1348 truorfal 1384 falortru 1385 truimfal 1388 nftru 1442 euotd 4171 rabxfr 4386 reuhyp 4388 elabrex 5652 caovcl 5918 caovass 5924 caovdi 5943 ectocl 6489 reef11 11395 bj-sbimeh 12968 bdtru 13019 bj-nn0suc0 13137 |
Copyright terms: Public domain | W3C validator |