| 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 2067 vextru 2721 rextru 3077 rabtru 3689 ss2abi 4067 ab0orv 4383 disjprg 5139 reusv2lem5 5402 rabxfr 5418 reuhyp 5420 euotd 5518 mptexgf 7242 elabrex 7262 elabrexg 7263 caovcl 7627 caovass 7633 caovdi 7652 ectocl 8825 fin1a2lem10 10449 riotaneg 12247 zriotaneg 12731 cshwsexaOLD 14863 eflt 16153 efgi0 19738 efgi1 19739 0frgp 19797 mpomulcn 24891 iundisj2 25584 pige3ALT 26562 tanord1 26579 tanord 26580 logtayl 26702 n0sind 28337 nnsind 28363 iundisj2f 32603 iundisj2fi 32799 ordtconn 33924 tgoldbachgt 34678 nexntru 36405 bj-fal 36571 bj-axd2d 36594 bj-rabtr 36931 bj-rabtrALT 36932 bj-dfid2ALT 37066 bj-finsumval0 37286 wl-impchain-mp-x 37448 wl-impchain-com-1.x 37452 wl-impchain-com-n.m 37457 wl-impchain-a1-x 37461 wl-moteq 37515 ftc1anclem5 37704 lhpexle1 40010 3lexlogpow5ineq2 42056 3lexlogpow2ineq1 42059 3lexlogpow2ineq2 42060 mzpcompact2lem 42762 ifpdfor 43478 ifpim1 43482 ifpnot 43483 ifpid2 43484 ifpim2 43485 uun0.1 44798 uunT1 44800 un10 44808 un01 44809 dfbi1ALTa 44960 simprimi 44961 n0abso 44993 liminfvalxr 45798 ovn02 46583 rmotru 48723 reutru 48724 |
| Copyright terms: Public domain | W3C validator |