Description: An inference version of
the transitive laws for implication imim2 56 and
imim1 81 (and imim1i 61 and imim2i 16), 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." Its
associated inference is mp2b 10.
(A bit of trivia: this is the most commonly referenced assertion in our
database (13449 times as of 22-Jul-2021). In second place is eqid 2610
(9597 times), followed by adantr 480 (8861 times), syl2anc 691 (7421 times),
adantl 481 (6403 times), and simpr 476
(5829 times). The Metamath program
command 'show usage' shows the number of references.)
(Contributed by NM, 30-Sep-1992.) (Proof shortened by Mel L. O'Cat,
20-Oct-2011.) (Proof shortened by Wolf Lammen,
26-Jul-2012.) |