Theorem pm4.71da

Deduction converting a biconditional to a biconditional with conjunction. Variant of pm4.71d. (Contributed by Zhi Wang, 30-Aug-2024.)

Hypothesis

pm4.71da.1

\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)

Conclusion

\( \vdash \varphi \rightarrow (\psi \leftrightarrow \psi \wedge \chi) \)

Proof

pm4.71da.1

biimpd _

pm4.71d _