| Description: An inference version of
the transitive laws for implication imim2 17 and
imim1 18, which Russell and Whitehead call "the
principle of the
syllogism...because...the syllogism in Barbara is derived from
them"
(quote after Theorem *2.06 of [WhiteheadRussell] p. 101). Some authors
call this law a "hypothetical syllogism." (The proof was
shortened by
O'Cat, 20-Oct-2011.)
(A bit of trivia: this is the most commonly referenced assertion in our
database. In second place is ax-mp 7, followed by visset 2128, bitri 189,
imp 375, and ex 400. The Metamath program command 'show
usage' shows the
number of references.) |