Description: Theorem *3.31 (Imp) of WhiteheadRussell p. 112. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 24-Mar-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | pm3.31 | |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph /\ ps ) -> ch ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | |- ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ch ) ) ) |
|
2 | 1 | impd | |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph /\ ps ) -> ch ) ) |