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 1531 | . 2 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) | |
3 | 1, 2 | mpbir 232 | 1 ⊢ ⊤ |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1526 = wceq 1528 ⊤wtru 1529 |
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 208 df-tru 1531 |
This theorem is referenced by: dftru2 1533 trut 1534 mptru 1535 tbtru 1536 bitru 1537 trud 1538 truan 1539 fal 1542 truorfal 1566 falortru 1567 trunortruOLD 1578 trunorfalOLD 1580 cadtru 1612 nftru 1796 altru 1799 extru 1971 sbtru 2063 vextru 2803 rabtru 3674 disjprgw 5052 disjprg 5053 reusv2lem5 5293 rabxfr 5309 reuhyp 5311 euotd 5394 elabrex 6993 caovcl 7331 caovass 7337 caovdi 7356 ectocl 8354 fin1a2lem10 9819 riotaneg 11608 zriotaneg 12084 cshwsexa 14174 eflt 15458 efgi0 18775 efgi1 18776 0frgp 18834 iundisj2 24077 pige3ALT 25032 tanord1 25048 tanord 25049 logtayl 25170 iundisj2f 30268 iundisj2fi 30446 ordtconn 31067 tgoldbachgt 31833 nexntru 33649 bj-axd2d 33824 bj-rabtr 34145 bj-rabtrALT 34146 bj-df-v 34241 bj-finsumval0 34455 wl-impchain-mp-x 34610 wl-impchain-com-1.x 34614 wl-impchain-com-n.m 34619 wl-impchain-a1-x 34623 wl-moteq 34636 ftc1anclem5 34852 lhpexle1 37024 mzpcompact2lem 39226 ifpdfor 39708 ifpim1 39712 ifpnot 39713 ifpid2 39714 ifpim2 39715 uun0.1 40989 uunT1 40991 un10 40999 un01 41000 elabrexg 41180 liminfvalxr 41940 ovn02 42727 |
Copyright terms: Public domain | W3C validator |