Description: Biconditional form of e2 . imbitrdi is e2bi without virtual deductions. (Contributed by Alan Sare, 10-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)