Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  bitru Structured version   Visualization version   GIF version

Theorem bitru 1547
 Description: A theorem is equivalent to truth. (Contributed by Mario Carneiro, 9-May-2015.)
Hypothesis
Ref Expression
bitru.1 𝜑
Assertion
Ref Expression
bitru (𝜑 ↔ ⊤)

Proof of Theorem bitru
StepHypRef Expression
1 bitru.1 . 2 𝜑
2 tru 1542 . 2
31, 22th 267 1 (𝜑 ↔ ⊤)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209  ⊤wtru 1539 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 1541 This theorem is referenced by:  truimtru  1561  falimtru  1563  falimfal  1564  notfal  1566  trubitru  1567  falbifal  1570  truorfal  1576  falortru  1577  exists1  2682  dfv2  3412  0frgp  18972  tgcgr4  26424  wl-2mintru1  35187  astbstanbst  43868  atnaiana  43882  dandysum2p2e4  43957
 Copyright terms: Public domain W3C validator