Theorem
biidd
Principle of identity with antecedent. (Contributed by NM, 25-Nov-1995.)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \psi) \)
Proof
biid
a1i
_
This is the content in the right pane.