This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem notnotrALT

Description: Converse of double negation. Alternate proof of notnotr . This proof is notnotrALTVD automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	notnotrALT	$⊢ \neg \neg φ \to φ$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ \neg \neg φ \to \neg \neg φ$
2		pm2.21	$⊢ \neg \neg φ \to (\neg φ \to \neg \neg \neg φ)$
3	1 2	mt4d	$⊢ \neg \neg φ \to φ$