Theorem imbi12

Closed form of imbi12i. Was automatically derived from its "Virtual Deduction" version and the Metamath program "MM-PA> MINIMIZE__WITH *" command. (Contributed by Alan Sare, 18-Mar-2012.)

Conclusion
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow (\chi \leftrightarrow \theta) \rightarrow (\varphi \rightarrow \chi \leftrightarrow \psi \rightarrow \theta) \)
Proof
l0
simplim
simprim
imbi12d l0 _
expi _