Theorem
anidmdbi
Conjunction idempotence with antecedent. (Contributed by Roy F. Longton, 8-Aug-2005.)
Conclusion
\( \vdash \varphi \rightarrow \psi \wedge \psi \leftrightarrow \varphi \rightarrow \psi \)
Proof
anidm
imbi2i
_
This is the content in the right pane.