Description: Syllogism inference with commutation of antecedents. (Contributed by NM, 29-Aug-2004) (Proof shortened by Mel L. O'Cat, 2-Feb-2006) (Proof shortened by Stefan Allan, 23-Feb-2006)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | sylcom.1 | |- ( ph -> ( ps -> ch ) ) |
|
| sylcom.2 | |- ( ps -> ( ch -> th ) ) |
||
| Assertion | sylcom | |- ( ph -> ( ps -> th ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sylcom.1 | |- ( ph -> ( ps -> ch ) ) |
|
| 2 | sylcom.2 | |- ( ps -> ( ch -> th ) ) |
|
| 3 | 2 | a2i | |- ( ( ps -> ch ) -> ( ps -> th ) ) |
| 4 | 1 3 | syl | |- ( ph -> ( ps -> th ) ) |