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

Metamath Proof Explorer

Theorem pm2.13

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

		Ref	Expression
	Assertion	pm2.13	$⊢ (φ \lor \neg \neg \neg φ)$

Step	Hyp	Ref	Expression
1		notnot	$⊢ \neg φ \to \neg \neg \neg φ$
2	1	orri	$⊢ (φ \lor \neg \neg \neg φ)$