![]() |
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 1356 | . 2 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) | |
3 | 1, 2 | mpbir 146 | 1 ⊢ ⊤ |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1351 = wceq 1353 ⊤wtru 1354 |
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 1356 |
This theorem is referenced by: fal 1360 dftru2 1361 mptru 1362 tbtru 1363 bitru 1365 a1tru 1369 truan 1370 truorfal 1406 falortru 1407 truimfal 1410 nftru 1466 euotd 4250 rabxfr 4466 reuhyp 4468 elabrex 5752 caovcl 6022 caovass 6028 caovdi 6047 ectocl 6595 reef11 11678 bj-sbimeh 14146 bdtru 14206 bj-nn0suc0 14324 |
Copyright terms: Public domain | W3C validator |