Theorem biadani

Inference associated with biadan. (Contributed by BJ, 4-Mar-2023.)

Hypothesis
biadani.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \psi \rightarrow (\varphi \leftrightarrow \chi) \leftrightarrow (\varphi \leftrightarrow \psi \wedge \chi) \)
Proof
l0
biadani.1
\( \vdash \varphi \rightarrow \psi \)
biadan
\( \vdash \varphi \rightarrow \psi \leftrightarrow (\psi \rightarrow (\varphi \leftrightarrow \chi) \leftrightarrow (\varphi \leftrightarrow \psi \wedge \chi)) \)
mpbi l0 _