Theorem imbibi

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.) (Proof shortened by Garrett Katz, 15-Jun-2026.)

Conclusion
\( \vdash (\varphi \rightarrow \psi \leftrightarrow \chi) \rightarrow \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Proof
l0
bitr3
\( \vdash (\varphi \rightarrow \psi \leftrightarrow \psi) \rightarrow (\varphi \rightarrow \psi \leftrightarrow \chi) \rightarrow (\psi \leftrightarrow \chi) \)
pm5.5
\( \vdash \varphi \rightarrow (\varphi \rightarrow \psi \leftrightarrow \psi) \)
syl11 l0 _