Theorem
biimt
A wff is equivalent to itself with true antecedent. (Contributed by NM, 28-Jan-1996.)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \varphi \rightarrow \psi) \)
Proof
l0
ax-1
pm2.27
impbid2
l0
_
This is the content in the right pane.