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

Metamath Proof Explorer

Theorem pm4.82

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

		Ref	Expression
	Assertion	pm4.82	$⊢ ((φ \to ψ) \land (φ \to \neg ψ)) \leftrightarrow \neg φ$

Step	Hyp	Ref	Expression
1		pm2.65	$⊢ (φ \to ψ) \to ((φ \to \neg ψ) \to \neg φ)$
2	1	imp	$⊢ ((φ \to ψ) \land (φ \to \neg ψ)) \to \neg φ$
3		pm2.21	$⊢ \neg φ \to (φ \to ψ)$
4		pm2.21	$⊢ \neg φ \to (φ \to \neg ψ)$
5	3 4	jca	$⊢ \neg φ \to ((φ \to ψ) \land (φ \to \neg ψ))$
6	2 5	impbii	$⊢ ((φ \to ψ) \land (φ \to \neg ψ)) \leftrightarrow \neg φ$