| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > tru | Structured version Visualization version GIF version | ||
| Description: The truth value ⊤ is provable. (Contributed by Anthony Hart, 13-Oct-2010.) |
| Ref | Expression |
|---|---|
| tru | ⊢ ⊤ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id 22 | . 2 ⊢ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥) | |
| 2 | df-tru 1543 | . 2 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) | |
| 3 | 1, 2 | mpbir 231 | 1 ⊢ ⊤ |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∀wal 1538 = wceq 1540 ⊤wtru 1541 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-tru 1543 |
| This theorem is referenced by: dftru2 1545 trut 1546 mptru 1547 tbtru 1548 bitru 1549 trud 1550 truan 1551 fal 1554 truorfal 1578 falortru 1579 cadtru 1620 nftru 1804 altru 1807 extru 1975 sbtru 2068 vextru 2714 rextru 3060 rabtru 3645 ss2abi 4019 ab0orv 4334 disjprg 5088 reusv2lem5 5341 rabxfr 5357 reuhyp 5359 euotd 5456 mptexgf 7158 elabrex 7178 elabrexg 7179 caovcl 7543 caovass 7549 caovdi 7568 ectocl 8710 fin1a2lem10 10303 riotaneg 12104 zriotaneg 12589 cshwsexaOLD 14731 eflt 16026 efgi0 19599 efgi1 19600 0frgp 19658 mpomulcn 24756 iundisj2 25448 pige3ALT 26427 tanord1 26444 tanord 26445 logtayl 26567 n0sind 28230 nnsind 28267 iundisj2f 32534 iundisj2fi 32741 ordtconn 33898 tgoldbachgt 34637 nexntru 36388 bj-fal 36554 bj-axd2d 36577 bj-rabtr 36914 bj-rabtrALT 36915 bj-dfid2ALT 37049 bj-finsumval0 37269 wl-impchain-mp-x 37431 wl-impchain-com-1.x 37435 wl-impchain-com-n.m 37440 wl-impchain-a1-x 37444 wl-moteq 37498 ftc1anclem5 37687 lhpexle1 39997 3lexlogpow5ineq2 42038 3lexlogpow2ineq1 42041 3lexlogpow2ineq2 42042 mzpcompact2lem 42734 ifpdfor 43448 ifpim1 43452 ifpnot 43453 ifpid2 43454 ifpim2 43455 uun0.1 44761 uunT1 44763 un10 44771 un01 44772 dfbi1ALTa 44923 simprimi 44924 n0abso 44960 liminfvalxr 45774 ovn02 46559 rmotru 48797 reutru 48798 |
| Copyright terms: Public domain | W3C validator |