Theorem pm4.8

Description: Theorem *4.8 of WhiteheadRussell p. 122. (Contributed by NM, 3-Jan-2005)

	Ref	Expression
Assertion	pm4.8	$$⊢\left(\phi \to \neg \phi \right)\leftrightarrow \neg \phi$$

Proof

Step	Hyp	Ref	Expression
1		pm2.01	$$⊢\left(\phi \to \neg \phi \right)\to \neg \phi$$
2		ax-1	$$⊢\neg \phi \to \left(\phi \to \neg \phi \right)$$
3	1 2	impbii	$$⊢\left(\phi \to \neg \phi \right)\leftrightarrow \neg \phi$$