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 ) ) |