Theorem tbt

A wff is equivalent to its equivalence with a truth. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)

Hypothesis
tbt.1
\( \vdash \varphi \)
Conclusion
\( \vdash \psi \leftrightarrow (\psi \leftrightarrow \varphi) \)
Proof
l0
tbt.1
\( \vdash \varphi \)
ibibr
pm5.74ri _
\( \vdash \varphi \rightarrow (\psi \leftrightarrow (\psi \leftrightarrow \varphi)) \)
ax-mp l0 _