Theorem bianir

A closed form of mpbir, analogous to pm2.27 (assertion). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Roger Witte, 17-Aug-2020.)

Conclusion

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

Proof

biimpr

impcom _