Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
True and false constants
The true constant
bitru
Next ⟩
trud
Metamath Proof Explorer
Ascii
Structured
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
⊢
(
𝜑
↔ ⊤ )