This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bj-dfnnf2

Description: Alternate definition of df-bj-nnf using only primitive symbols ( -> , -. , A. ) in each conjunct. (Contributed by BJ, 20-Aug-2023)

		Ref	Expression
	Assertion	bj-dfnnf2	$⊢ Ⅎ' x φ \leftrightarrow ((φ \to \forall x φ) \land (\neg φ \to \forall x \neg φ))$

Step	Hyp	Ref	Expression
1		df-bj-nnf	$⊢ Ⅎ' x φ \leftrightarrow ((\exists x φ \to φ) \land (φ \to \forall x φ))$
2		eximal	$⊢ (\exists x φ \to φ) \leftrightarrow (\neg φ \to \forall x \neg φ)$
3	2	anbi2ci	$⊢ ((\exists x φ \to φ) \land (φ \to \forall x φ)) \leftrightarrow ((φ \to \forall x φ) \land (\neg φ \to \forall x \neg φ))$
4	1 3	bitri	$⊢ Ⅎ' x φ \leftrightarrow ((φ \to \forall x φ) \land (\neg φ \to \forall x \neg φ))$