Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > tru | Structured version Visualization version Unicode 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 1486 | . 2 | |
3 | 1, 2 | mpbir 221 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wal 1481 wceq 1483 wtru 1484 |
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 197 df-tru 1486 |
This theorem is referenced by: fal 1490 dftru2 1491 trut 1492 trud 1493 tbtru 1494 bitru 1496 a1tru 1500 truan 1501 truorfal 1511 falortru 1512 cadtru 1559 nftru 1730 rabtru 3361 disjprg 4648 reusv2lem5 4873 rabxfr 4890 reuhyp 4896 euotd 4975 elabrex 6501 caovcl 6828 caovass 6834 caovdi 6853 ectocl 7815 fin1a2lem10 9231 riotaneg 11002 zriotaneg 11491 cshwsexa 13570 eflt 14847 efgi0 18133 efgi1 18134 0frgp 18192 iundisj2 23317 pige3 24269 tanord1 24283 tanord 24284 logtayl 24406 iundisj2f 29403 iundisj2fi 29556 ordtconn 29971 tgoldbachgt 30741 allt 32400 nextnt 32404 bj-axd2d 32577 bj-extru 32654 bj-rabtr 32926 bj-rabtrALT 32927 bj-rabtrALTALT 32928 bj-df-v 33016 bj-finsumval0 33147 wl-impchain-mp-x 33269 wl-impchain-com-1.x 33273 wl-impchain-com-n.m 33278 wl-impchain-a1-x 33282 ftc1anclem5 33489 lhpexle1 35294 mzpcompact2lem 37314 ifpdfor 37809 ifpim1 37813 ifpnot 37814 ifpid2 37815 ifpim2 37816 uun0.1 39005 uunT1 39007 un10 39015 un01 39016 elabrexg 39206 liminfvalxr 40015 ovn02 40782 |
Copyright terms: Public domain | W3C validator |