Axiom ax-frege28 40174

Description: Contraposition. Identical to con3 156. 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	⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))

Detailed syntax breakdown of Axiom ax-frege28

Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2		wps	. 2 wff 𝜓
3	2	wn 3	. . 3 wff ¬ 𝜓
4	1	wn 3	. . 3 wff ¬ 𝜑
5	3, 4	wi 4	. 2 wff (¬ 𝜓 → ¬ 𝜑)
6	1, 2, 5	bj-0 33881	1 wff ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))

This axiom is referenced by:  frege29  40175  frege33  40180  frege54cor0a  40207