Description: A mixed syllogism inference from two biconditionals.

Note on the various syllogism-like statements in set.mm. The
hypothetical syllogism syl infers an implication from two implications
(and there are 3syl and 4syl for chaining more inferences). There
are four inferences inferring an implication from one implication and
one biconditional: sylbi , sylib , sylbir , sylibr ; four
inferences inferring an implication from two biconditionals: sylbb ,
sylbbr , sylbb1 , sylbb2 ; four inferences inferring a
biconditional from two biconditionals: bitri , bitr2i , bitr3i ,
bitr4i (and more for chaining more biconditionals). There are also
closed forms and deduction versions of these, like, among many others,
syld , syl5 , syl6 , mpbid , bitrd , syl5bb , bitrdi and
variants. (Contributed by BJ, 21-Apr-2019)