Theorem bj-nnfan

Description: Nonfreeness in both conjuncts implies nonfreeness in the conjunction. (Contributed by BJ, 19-Nov-2023) In classical logic, there is a proof using the definition of conjunction in terms of implication and negation, so using bj-nnfim , bj-nnfnt and bj-nnfbi , but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-nnfan	|- ( ( F// x ph /\ F// x ps ) -> F// x ( ph /\ ps ) )

Proof

Step	Hyp	Ref	Expression
1		df-bj-nnf	|- ( F// x ph <-> ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) )
2		df-bj-nnf	|- ( F// x ps <-> ( ( E. x ps -> ps ) /\ ( ps -> A. x ps ) ) )
3		19.40	|- ( E. x ( ph /\ ps ) -> ( E. x ph /\ E. x ps ) )
4		anim12	|- ( ( ( E. x ph -> ph ) /\ ( E. x ps -> ps ) ) -> ( ( E. x ph /\ E. x ps ) -> ( ph /\ ps ) ) )
5	3 4	syl5	|- ( ( ( E. x ph -> ph ) /\ ( E. x ps -> ps ) ) -> ( E. x ( ph /\ ps ) -> ( ph /\ ps ) ) )
6		anim12	|- ( ( ( ph -> A. x ph ) /\ ( ps -> A. x ps ) ) -> ( ( ph /\ ps ) -> ( A. x ph /\ A. x ps ) ) )
7		id	|- ( ( ph /\ ps ) -> ( ph /\ ps ) )
8	7	alanimi	|- ( ( A. x ph /\ A. x ps ) -> A. x ( ph /\ ps ) )
9	6 8	syl6	|- ( ( ( ph -> A. x ph ) /\ ( ps -> A. x ps ) ) -> ( ( ph /\ ps ) -> A. x ( ph /\ ps ) ) )
10	5 9	anim12i	|- ( ( ( ( E. x ph -> ph ) /\ ( E. x ps -> ps ) ) /\ ( ( ph -> A. x ph ) /\ ( ps -> A. x ps ) ) ) -> ( ( E. x ( ph /\ ps ) -> ( ph /\ ps ) ) /\ ( ( ph /\ ps ) -> A. x ( ph /\ ps ) ) ) )
11	10	an4s	|- ( ( ( ( E. x ph -> ph ) /\ ( ph -> A. x ph ) ) /\ ( ( E. x ps -> ps ) /\ ( ps -> A. x ps ) ) ) -> ( ( E. x ( ph /\ ps ) -> ( ph /\ ps ) ) /\ ( ( ph /\ ps ) -> A. x ( ph /\ ps ) ) ) )
12	1 2 11	syl2anb	|- ( ( F// x ph /\ F// x ps ) -> ( ( E. x ( ph /\ ps ) -> ( ph /\ ps ) ) /\ ( ( ph /\ ps ) -> A. x ( ph /\ ps ) ) ) )
13		df-bj-nnf	|- ( F// x ( ph /\ ps ) <-> ( ( E. x ( ph /\ ps ) -> ( ph /\ ps ) ) /\ ( ( ph /\ ps ) -> A. x ( ph /\ ps ) ) ) )
14	12 13	sylibr	|- ( ( F// x ph /\ F// x ps ) -> F// x ( ph /\ ps ) )