Theorem bian1d

Adding a superfluous conjunct in a biconditional. (Contributed by Thierry Arnoux, 26-Feb-2017.) (Proof shortened by Hongxiu Chen, 29-Jun-2025.) (Proof shortened by Peter Mazsa, 24-Feb-2026.)

Hypothesis

bian1d.1

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

Conclusion

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

Proof

bian1d.1

baibd _

pm5.32da _