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

Metamath Proof Explorer

Theorem con1bii

Description: A contraposition inference. (Contributed by NM, 12-Mar-1993) (Proof shortened by Wolf Lammen, 13-Oct-2012)

		Ref	Expression
	Hypothesis	con1bii.1	$⊢ \neg φ \leftrightarrow ψ$
	Assertion	con1bii	$⊢ \neg ψ \leftrightarrow φ$

Step	Hyp	Ref	Expression
1		con1bii.1	$⊢ \neg φ \leftrightarrow ψ$
2		notnotb	$⊢ φ \leftrightarrow \neg \neg φ$
3	2 1	xchbinx	$⊢ φ \leftrightarrow \neg ψ$
4	3	bicomi	$⊢ \neg ψ \leftrightarrow φ$