Metamath Proof Explorer


Axiom ax-frege28

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

Detailed syntax breakdown

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