imnand2

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

Step	Hyp	Ref	Expression
1		nannot	$⊢ \neg φ \leftrightarrow (φ ⊼ φ)$
2		nannot	$⊢ \neg ψ \leftrightarrow (ψ ⊼ ψ)$
3	1 2	anbi12i	$⊢ (\neg φ \land \neg ψ) \leftrightarrow ((φ ⊼ φ) \land (ψ ⊼ ψ))$
4	3	notbii	$⊢ \neg (\neg φ \land \neg ψ) \leftrightarrow \neg ((φ ⊼ φ) \land (ψ ⊼ ψ))$
5		iman	$⊢ (\neg φ \to ψ) \leftrightarrow \neg (\neg φ \land \neg ψ)$
6		df-nan	$⊢ ((φ ⊼ φ) ⊼ (ψ ⊼ ψ)) \leftrightarrow \neg ((φ ⊼ φ) \land (ψ ⊼ ψ))$
7	4 5 6	3bitr4i	$⊢ (\neg φ \to ψ) \leftrightarrow ((φ ⊼ φ) ⊼ (ψ ⊼ ψ))$

Metamath Proof Explorer