Description: Contraposition. Identical to con3 . Theorem *2.16 of WhiteheadRussell p. 103. Axiom 28 of Frege1879 p. 43. (Contributed by RP, 24-Dec-2019) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-frege28 | |- ( ( ph -> ps ) -> ( -. ps -> -. ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | wph | |- ph |
|
| 1 | wps | |- ps |
|
| 2 | 0 1 | wi | |- ( ph -> ps ) |
| 3 | 1 | wn | |- -. ps |
| 4 | 0 | wn | |- -. ph |
| 5 | 3 4 | wi | |- ( -. ps -> -. ph ) |
| 6 | 2 5 | wi | |- ( ( ph -> ps ) -> ( -. ps -> -. ph ) ) |