Theorem dfnan2

Description: Alternative denial in terms of our primitive connectives (implication and negation). (Contributed by WL, 26-Jun-2020)

	Ref	Expression
Assertion	dfnan2	$$⊢\left(\phi ⊼\psi \right)\leftrightarrow \left(\phi \to \neg \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		df-nan	$$⊢\left(\phi ⊼\psi \right)\leftrightarrow \neg \left(\phi \wedge \psi \right)$$
2		imnan	$$⊢\left(\phi \to \neg \psi \right)\leftrightarrow \neg \left(\phi \wedge \psi \right)$$
3	1 2	bitr4i	$$⊢\left(\phi ⊼\psi \right)\leftrightarrow \left(\phi \to \neg \psi \right)$$