Theorem 3biant1d

A conjunction is equivalent to a threefold conjunction with single truth, analogous to biantrud. (Contributed by Alexander van der Vekens, 26-Sep-2017.)

Hypothesis
3biantd.1
\( \vdash \varphi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow (\chi \wedge \psi \leftrightarrow \theta \wedge \chi \wedge \psi) \)
Proof
3biantd.1
l1
biantrurd _
\( \vdash \varphi \rightarrow (\chi \wedge \psi \leftrightarrow \theta \wedge (\chi \wedge \psi)) \)
3anass
\( \vdash \theta \wedge \chi \wedge \psi \leftrightarrow \theta \wedge (\chi \wedge \psi) \)
bitr4di l1 _