Metamath Proof Explorer

Theorem notbi

Description: Contraposition. Theorem *4.11 of WhiteheadRussell p. 117. (Contributed by NM, 21-May-1994) (Proof shortened by Wolf Lammen, 12-Jun-2013)

		Ref	Expression
	Assertion	notbi	$⊢ (φ \leftrightarrow ψ) \leftrightarrow (\neg φ \leftrightarrow \neg ψ)$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ (φ \leftrightarrow ψ) \to (φ \leftrightarrow ψ)$
2	1	notbid	$⊢ (φ \leftrightarrow ψ) \to (\neg φ \leftrightarrow \neg ψ)$
3		id	$⊢ (\neg φ \leftrightarrow \neg ψ) \to (\neg φ \leftrightarrow \neg ψ)$
4	3	con4bid	$⊢ (\neg φ \leftrightarrow \neg ψ) \to (φ \leftrightarrow ψ)$
5	2 4	impbii	$⊢ (φ \leftrightarrow ψ) \leftrightarrow (\neg φ \leftrightarrow \neg ψ)$

	
		OSZAR »