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 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 2622
(9597 times), followed by adantr 481 (8861 times), syl2anc 693 (7421 times),
adantl 482 (6403 times), and simpr 477
(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.) |