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 
|- ph
Assertion bitru 
|- ( ph <-> T. )

Proof

Step Hyp Ref Expression
1 bitru.1 
 |-  ph
2 tru 
 |-  T.
3 1 2 2th 
 |-  ( ph <-> T. )