Theorem biadaniALT

Alternate proof of biadani not using biadan. (Contributed by BJ, 4-Mar-2023.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis
biadani.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \psi \rightarrow (\varphi \leftrightarrow \chi) \leftrightarrow (\varphi \leftrightarrow \psi \wedge \chi) \)
Proof
l0
pm5.32
\( \vdash \psi \rightarrow (\varphi \leftrightarrow \chi) \leftrightarrow (\psi \wedge \varphi \leftrightarrow \psi \wedge \chi) \)
biadani.1
pm4.71ri _
bibi1i _
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \leftrightarrow (\psi \wedge \varphi \leftrightarrow \psi \wedge \chi) \)
bitr4i l0 _