Description: An inference version of
the transitive laws for implication imim2 58 and
imim1 83 (and imim1i 63 and imim2i 16), which Russell and Whitehead call
"the principle of the syllogism ... because ... the syllogism in
Barbara
is derived from [syl 17]" (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 2738
(9597 times), followed by adantr 480 (8861 times), syl2anc 583 (7421 times),
adantl 481 (6403 times), and simpr 484
(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.) |