Description: Theorem *2.65 of WhiteheadRussell p. 107. Proof by contradiction. (Contributed by NM, 21-Jun-1993) (Proof shortened by Wolf Lammen, 8-Mar-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | pm2.65 | |- ( ( ph -> ps ) -> ( ( ph -> -. ps ) -> -. ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | idd | |- ( ( ph -> ps ) -> ( -. ph -> -. ph ) ) |
|
| 2 | con3 | |- ( ( ph -> ps ) -> ( -. ps -> -. ph ) ) |
|
| 3 | 1 2 | jad | |- ( ( ph -> ps ) -> ( ( ph -> -. ps ) -> -. ph ) ) |