Theorem abab

Introduce one conjunct as equivalent to the other. "abab" stands for "and, biconditional, and, biconditional". (Contributed by Wolf Lammen, 4-Jun-2026.)

Conclusion
\( \vdash \varphi \wedge \psi \leftrightarrow \varphi \wedge (\varphi \leftrightarrow \psi) \)
Proof
l0
simpl
pm5.1
l2
jca l0 _
biimp
l4
anim2i _
\( \vdash \varphi \wedge (\varphi \leftrightarrow \psi) \rightarrow \varphi \wedge (\varphi \rightarrow \psi) \)
abai
\( \vdash \varphi \wedge \psi \leftrightarrow \varphi \wedge (\varphi \rightarrow \psi) \)
sylibr l4 _
impbii l2 _