New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > tru | Unicode version |
Description: is provable. (Contributed by Anthony Hart, 13-Oct-2010.) |
Ref | Expression |
---|---|
tru |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biid 227 | . 2 | |
2 | df-tru 1319 | . 2 | |
3 | 1, 2 | mpbir 200 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 176 wtru 1316 |
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 177 df-tru 1319 |
This theorem is referenced by: fal 1322 trud 1323 tbtru 1324 bitru 1326 a1tru 1330 truorfal 1341 falortru 1342 truimfal 1345 cadtru 1401 nftru 1554 cbv3 1982 finds 4411 caovcl 5623 caovass 5627 caovdi 5634 ectocl 5992 |
Copyright terms: Public domain | W3C validator |