Axiom ax-frege28 38124

Description: Contraposition. Identical to con3 149. Theorem *2.16 of [WhiteheadRussell] p. 103. Axiom 28 of [Frege1879] p. 43. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-frege28	|- ( ( ph -> ps ) -> ( -. ps -> -. ph ) )

Detailed syntax breakdown of Axiom ax-frege28

Step	Hyp	Ref	Expression
1		wph	. 2 wff ph
2		wps	. 2 wff ps
3	2	wn 3	. . 3 wff -. ps
4	1	wn 3	. . 3 wff -. ph
5	3, 4	wi 4	. 2 wff ( -. ps -> -. ph )
6	1, 2, 5	bj-0 32533	1 wff ( ( ph -> ps ) -> ( -. ps -> -. ph ) )

This axiom is referenced by:  frege29  38125  frege33  38130  frege54cor0a  38157