Description: A closed form of syllogism (see syl ). Theorem *2.05 of WhiteheadRussell p. 100. Its associated inference is imim2i . Its associated deduction is imim2d . An alternate proof from more basic results is given by ax-1 followed by a2d . (Contributed by NM, 29-Dec-1992) (Proof shortened by Wolf Lammen, 6-Sep-2012)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | imim2 | |- ( ( ph -> ps ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | |- ( ( ph -> ps ) -> ( ph -> ps ) ) |
|
| 2 | 1 | imim2d | |- ( ( ph -> ps ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) ) |