| Description: An inference version of
the transitive laws for implication imim2 59 and
imim1 84 (and imim1i 64 and imim2i 17), which Russell and Whitehead call
"the principle of the syllogism ... because ... the syllogism in
Barbara
[barbara 2692] is derived from [syl 18]" (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 2765
(9597 times), followed by adantr 485 (8861 times), syl2anc 595 (7421 times),
adantl 486 (6403 times), and simpr 489
(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.) |