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	$$⊢\left(\phi \to \psi \right)\to \left(\neg \psi \to \neg \phi \right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	$$wff\phi$$
1		wps	$$wff\psi$$
2	0 1	wi	$$wff\left(\phi \to \psi \right)$$
3	1	wn	$$wff\neg \psi$$
4	0	wn	$$wff\neg \phi$$
5	3 4	wi	$$wff\left(\neg \psi \to \neg \phi \right)$$
6	2 5	wi	$$wff\left(\left(\phi \to \psi \right)\to \left(\neg \psi \to \neg \phi \right)\right)$$