Metamath Proof Explorer

Theorem nic-dfneg

Description: This theorem "defines" negation in terms of 'nand'. Analogous to nannot . In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to a definition ($a statement). (Contributed by NM, 11-Dec-2008) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	nic-dfneg	$⊢ (((φ ⊼ φ) ⊼ \neg φ) ⊼ (((φ ⊼ φ) ⊼ (φ ⊼ φ)) ⊼ (\neg φ ⊼ \neg φ)))$

Proof

Step	Hyp	Ref	Expression
1		nannot	$⊢ \neg φ \leftrightarrow (φ ⊼ φ)$
2	1	bicomi	$⊢ (φ ⊼ φ) \leftrightarrow \neg φ$
3		nanbi	$⊢ ((φ ⊼ φ) \leftrightarrow \neg φ) \leftrightarrow (((φ ⊼ φ) ⊼ \neg φ) ⊼ (((φ ⊼ φ) ⊼ (φ ⊼ φ)) ⊼ (\neg φ ⊼ \neg φ)))$
4	2 3	mpbi	$⊢ (((φ ⊼ φ) ⊼ \neg φ) ⊼ (((φ ⊼ φ) ⊼ (φ ⊼ φ)) ⊼ (\neg φ ⊼ \neg φ)))$