Description: An inference version of the transitive laws for implication imim2 and imim1 (and imim1i and imim2i ), which Russell and Whitehead call "the principle of the syllogism ... because ... the syllogism in Barbara is derived from [[ syl ]" (quote after Theorem *2.06 of WhiteheadRussell p. 101). Some authors call this law a "hypothetical syllogism". Its associated inference is mp2b .
(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 (9597 times), followed by adantr (8861 times), syl2anc (7421 times), adantl (6403 times), and simpr (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)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | syl.1 | |- ( ph -> ps ) |
|
| syl.2 | |- ( ps -> ch ) |
||
| Assertion | syl | |- ( ph -> ch ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | syl.1 | |- ( ph -> ps ) |
|
| 2 | syl.2 | |- ( ps -> ch ) |
|
| 3 | 2 | a1i | |- ( ph -> ( ps -> ch ) ) |
| 4 | 1 3 | mpd | |- ( ph -> ch ) |