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 1345 | . 2 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) | |
3 | 1, 2 | mpbir 145 | 1 ⊢ ⊤ |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1340 = wceq 1342 ⊤wtru 1343 |
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 1345 |
This theorem is referenced by: fal 1349 dftru2 1350 mptru 1351 tbtru 1352 bitru 1354 a1tru 1358 truan 1359 truorfal 1395 falortru 1396 truimfal 1399 nftru 1453 euotd 4226 rabxfr 4442 reuhyp 4444 elabrex 5720 caovcl 5987 caovass 5993 caovdi 6012 ectocl 6559 reef11 11626 bj-sbimeh 13494 bdtru 13555 bj-nn0suc0 13673 |
Copyright terms: Public domain | W3C validator |