Theorem bitr3

Closed nested implication form of bitr3i. Derived automatically from [bitr3VD]. (Contributed by Alan Sare, 31-Dec-2011.)

Conclusion

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

Proof

bibi1

biimpd _