|Description: A mixed syllogism
inference from two biconditionals.
Note on the various syllogism-like statements in set.mm. The
hypothetical syllogism syl 14 infers an implication from two implications
(and there are 3syl 17 and 4syl 18 for chaining more inferences). There
are four inferences inferring an implication from one implication and
one biconditional: sylbi 120, sylib 121, sylbir 134, sylibr 133; four
inferences inferring an implication from two biconditionals: sylbb 122,
sylbbr 135, sylbb1 136, sylbb2 137; four inferences inferring a
biconditional from two biconditionals: bitri 183, bitr2i 184, bitr3i 185,
bitr4i 186 (and more for chaining more biconditionals).
There are also
closed forms and deduction versions of these, like, among many others,
syld 45, syl5 32, syl6 33,
mpbid 146, bitrd 187, syl5bb 191, syl6bb 195 and
variants. (Contributed by BJ, 21-Apr-2019.)