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 121, sylib 122, sylbir 135, sylibr 134; four
inferences inferring an implication from two biconditionals: sylbb 123,
sylbbr 136, sylbb1 137, sylbb2 138; four inferences inferring a
biconditional from two biconditionals: bitri 184, bitr2i 185, bitr3i 186,
bitr4i 187 (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 147, bitrd 188, bitrid 192, bitrdi 196 and
variants. (Contributed by BJ, 21-Apr-2019.) |