![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > tru | Structured version Visualization version Unicode version |
Description: The truth value ![]() |
Ref | Expression |
---|---|
tru |
![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-tru 1447 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbir 213 |
1
![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
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 189 df-tru 1447 |
This theorem is referenced by: fal 1451 dftru2 1452 trud 1453 tbtru 1454 bitru 1456 a1tru 1460 truan 1461 truorfal 1471 falortru 1472 truimfal 1475 falbitru 1481 cadtru 1523 nftru 1677 disjprg 4398 reusv2lem5 4608 rabxfr 4622 reuhyp 4628 euotd 4702 elabrex 6148 caovcl 6463 caovass 6469 caovdi 6488 ectocl 7431 fin1a2lem10 8839 riotaneg 10586 zriotaneg 11049 cshwsexa 12923 eflt 14171 efgi0 17370 efgi1 17371 0frgp 17429 iundisj2 22502 pige3 23472 tanord1 23486 tanord 23487 logtayl 23605 rabtru 28135 iundisj2f 28200 iundisj2fi 28373 ordtcon 28731 allt 31061 nextnt 31065 bj-trut 31166 bj-axd2d 31176 bj-nftru 31199 bj-extru 31267 bj-rabtr 31533 bj-rabtrALT 31534 bj-rabtrALTALT 31535 bj-df-v 31620 bj-finsumval0 31702 wl-impchain-mp-x 31824 wl-impchain-com-1.x 31828 wl-impchain-com-n.m 31833 wl-impchain-a1-x 31837 ftc1anclem5 32021 lhpexle1 33573 mzpcompact2lem 35593 ifpdfor 36108 ifpim1 36112 ifpnot 36113 ifpid2 36114 ifpim2 36115 uun0.1 37165 uunT1 37167 un10 37175 un01 37176 elabrexg 37370 ovn02 38390 |
Copyright terms: Public domain | W3C validator |