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

Metamath Proof Explorer

Theorem dfbi1

Description: Relate the biconditional connective to primitive connectives. See dfbi1ALT for an unusual version proved directly from axioms. (Contributed by NM, 29-Dec-1992)

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

Proof

Step	Hyp	Ref	Expression
1		df-bi	$⊢ \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))$
2		impbi	$⊢ ((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to ((\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))))$
3	2	con3rr3	$⊢ \neg ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))$
4	1 3	mt3	$⊢ (φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))$