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	|- ( F// x ph <-> ( ( ph -> A. x ph ) /\ ( -. ph -> A. x -. ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-bj-nnf	|- ( F// x ph <-> ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) )
2		eximal	|- ( ( E. x ph -> ph ) <-> ( -. ph -> A. x -. ph ) )
3	2	anbi2ci	|- ( ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) <-> ( ( ph -> A. x ph ) /\ ( -. ph -> A. x -. ph ) ) )
4	1 3	bitri	|- ( F// x ph <-> ( ( ph -> A. x ph ) /\ ( -. ph -> A. x -. ph ) ) )