Obsolete version of imbibi as of 15-Jun-2026. The antecedent of one
side of a biconditional can be moved out of the biconditional to become
the antecedent of the remaining biconditional. (Contributed by BJ,
1-Jan-2025.) (Proof shortened by Wolf Lammen, 5-Jan-2025.)
(New usage is discouraged.) (Proof modification is discouraged.)
\( \vdash (\varphi \rightarrow \psi \leftrightarrow \chi) \rightarrow \varphi \rightarrow (\psi \leftrightarrow \chi) \)
\( \vdash \varphi \rightarrow \varphi \rightarrow \psi \leftrightarrow \varphi \rightarrow \psi \)
\( \vdash (\varphi \rightarrow \psi \leftrightarrow \chi) \rightarrow (\varphi \rightarrow \varphi \rightarrow \psi \leftrightarrow \varphi \rightarrow \chi) \)