Description: Version of mt2 where the major premise is a biconditional. Another proof is also possible via con2bii and mpbi . The current mt2bi should be relabeled, maybe to imfal. (Contributed by BJ, 5-Oct-2024)