Description: Join three logical equivalences to form equivalence of implications.
imbi13 is imbi13VD without virtual deductions and was automatically
derived from imbi13VD using the tools program
translate..without..overwriting.cmd and Metamath's minimize command.
(Contributed by Alan Sare, 18-Mar-2012)(Proof modification is discouraged.)(New usage is discouraged.)