![]() |
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 1544 | . 2 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) | |
3 | 1, 2 | mpbir 230 | 1 ⊢ ⊤ |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1539 = wceq 1541 ⊤wtru 1542 |
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 206 df-tru 1544 |
This theorem is referenced by: dftru2 1546 trut 1547 mptru 1548 tbtru 1549 bitru 1550 trud 1551 truan 1552 fal 1555 truorfal 1579 falortru 1580 cadtru 1622 nftru 1806 altru 1809 extru 1979 sbtru 2070 vextru 2721 rextru 3078 rabtru 3640 ss2abi 4021 ab0orv 4336 disjprgw 5098 disjprg 5099 reusv2lem5 5355 rabxfr 5371 reuhyp 5373 euotd 5468 mptexgf 7168 elabrex 7186 caovcl 7542 caovass 7548 caovdi 7567 ectocl 8682 fin1a2lem10 10303 riotaneg 12092 zriotaneg 12574 cshwsexaOLD 14671 eflt 15959 efgi0 19461 efgi1 19462 0frgp 19520 iundisj2 24865 pige3ALT 25828 tanord1 25845 tanord 25846 logtayl 25967 iundisj2f 31337 iundisj2fi 31526 ordtconn 32318 tgoldbachgt 33088 nexntru 34814 bj-fal 34972 bj-axd2d 34996 bj-rabtr 35338 bj-rabtrALT 35339 bj-dfid2ALT 35474 bj-finsumval0 35694 wl-impchain-mp-x 35856 wl-impchain-com-1.x 35860 wl-impchain-com-n.m 35865 wl-impchain-a1-x 35869 wl-moteq 35911 ftc1anclem5 36093 lhpexle1 38409 3lexlogpow5ineq2 40450 3lexlogpow2ineq1 40453 3lexlogpow2ineq2 40454 mzpcompact2lem 40983 ifpdfor 41648 ifpim1 41652 ifpnot 41653 ifpid2 41654 ifpim2 41655 uun0.1 42971 uunT1 42973 un10 42981 un01 42982 elabrexg 43160 liminfvalxr 43925 ovn02 44710 rmotru 46790 reutru 46791 |
Copyright terms: Public domain | W3C validator |