Metamath Proof Explorer

Theorem bijust

Description: Theorem used to justify the definition of the biconditional df-bi . Instance of bijust0 . (Contributed by NM, 11-May-1999)

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

Step	Hyp	Ref	Expression
1		bijust0	$⊢ \neg ((\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))))$