| 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 32740 ordtconn 33892 tgoldbachgt 34631 nexntru 36382 bj-fal 36548 bj-axd2d 36571 bj-rabtr 36908 bj-rabtrALT 36909 bj-dfid2ALT 37043 bj-finsumval0 37263 wl-impchain-mp-x 37425 wl-impchain-com-1.x 37429 wl-impchain-com-n.m 37434 wl-impchain-a1-x 37438 wl-moteq 37492 ftc1anclem5 37681 lhpexle1 39991 3lexlogpow5ineq2 42032 3lexlogpow2ineq1 42035 3lexlogpow2ineq2 42036 mzpcompact2lem 42728 ifpdfor 43442 ifpim1 43446 ifpnot 43447 ifpid2 43448 ifpim2 43449 uun0.1 44755 uunT1 44757 un10 44765 un01 44766 dfbi1ALTa 44917 simprimi 44918 n0abso 44954 liminfvalxr 45768 ovn02 46553 rmotru 48791 reutru 48792 |
| Copyright terms: Public domain | W3C validator |