This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 ↔ ⊤ )