Metamath Proof Explorer

Theorem nanbi

Description: Biconditional in terms of alternative denial. (Contributed by Jeff Hoffman, 19-Nov-2007) (Proof shortened by Wolf Lammen, 27-Jun-2020)

		Ref	Expression
	Assertion	nanbi	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ ⊼ ψ) ⊼ ((φ ⊼ φ) ⊼ (ψ ⊼ ψ)))$

Proof

Step	Hyp	Ref	Expression
1		dfbi3	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ \land ψ) \lor (\neg φ \land \neg ψ))$
2		df-or	$⊢ ((φ \land ψ) \lor (\neg φ \land \neg ψ)) \leftrightarrow (\neg (φ \land ψ) \to (\neg φ \land \neg ψ))$
3		df-nan	$⊢ (φ ⊼ ψ) \leftrightarrow \neg (φ \land ψ)$
4	3	bicomi	$⊢ \neg (φ \land ψ) \leftrightarrow (φ ⊼ ψ)$
5		nannot	$⊢ \neg φ \leftrightarrow (φ ⊼ φ)$
6		nannot	$⊢ \neg ψ \leftrightarrow (ψ ⊼ ψ)$
7	5 6	anbi12i	$⊢ (\neg φ \land \neg ψ) \leftrightarrow ((φ ⊼ φ) \land (ψ ⊼ ψ))$
8	4 7	imbi12i	$⊢ (\neg (φ \land ψ) \to (\neg φ \land \neg ψ)) \leftrightarrow ((φ ⊼ ψ) \to ((φ ⊼ φ) \land (ψ ⊼ ψ)))$
9	1 2 8	3bitri	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ ⊼ ψ) \to ((φ ⊼ φ) \land (ψ ⊼ ψ)))$
10		nannan	$⊢ ((φ ⊼ ψ) ⊼ ((φ ⊼ φ) ⊼ (ψ ⊼ ψ))) \leftrightarrow ((φ ⊼ ψ) \to ((φ ⊼ φ) \land (ψ ⊼ ψ)))$
11	9 10	bitr4i	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ ⊼ ψ) ⊼ ((φ ⊼ φ) ⊼ (ψ ⊼ ψ)))$