Metamath Proof Explorer


Theorem bitru

Description: A theorem is equivalent to truth. (Contributed by Mario Carneiro, 9-May-2015)

Ref Expression
Hypothesis bitru.1 𝜑
Assertion bitru ( 𝜑 ↔ ⊤ )

Proof

Step Hyp Ref Expression
1 bitru.1 𝜑
2 tru
3 1 2 2th ( 𝜑 ↔ ⊤ )