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 1546 | . 2 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) | |
3 | 1, 2 | mpbir 234 | 1 ⊢ ⊤ |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1541 = wceq 1543 ⊤wtru 1544 |
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 210 df-tru 1546 |
This theorem is referenced by: dftru2 1548 trut 1549 mptru 1550 tbtru 1551 bitru 1552 trud 1553 truan 1554 fal 1557 truorfal 1581 falortru 1582 trunortruOLD 1593 trunorfalOLD 1595 cadtru 1628 nftru 1812 altru 1815 extru 1984 sbtru 2073 vextru 2721 rabtru 3596 ss2abi 3977 ab0orv 4290 disjprgw 5045 disjprg 5046 reusv2lem5 5292 rabxfr 5308 reuhyp 5310 euotd 5393 elabrex 7053 caovcl 7399 caovass 7405 caovdi 7424 ectocl 8464 fin1a2lem10 10020 riotaneg 11808 zriotaneg 12288 cshwsexa 14386 eflt 15675 efgi0 19107 efgi1 19108 0frgp 19166 iundisj2 24443 pige3ALT 25406 tanord1 25423 tanord 25424 logtayl 25545 iundisj2f 30645 iundisj2fi 30835 ordtconn 31586 tgoldbachgt 32352 nexntru 34327 bj-fal 34485 bj-axd2d 34509 bj-rabtr 34852 bj-rabtrALT 34853 bj-finsumval0 35188 wl-impchain-mp-x 35352 wl-impchain-com-1.x 35356 wl-impchain-com-n.m 35361 wl-impchain-a1-x 35365 wl-moteq 35407 ftc1anclem5 35589 lhpexle1 37757 3lexlogpow5ineq2 39795 3lexlogpow2ineq1 39798 3lexlogpow2ineq2 39799 mzpcompact2lem 40274 ifpdfor 40755 ifpim1 40759 ifpnot 40760 ifpid2 40761 ifpim2 40762 uun0.1 42069 uunT1 42071 un10 42079 un01 42080 elabrexg 42260 liminfvalxr 42997 ovn02 43779 rextru 45820 rmotru 45821 reutru 45822 |
Copyright terms: Public domain | W3C validator |