Theorem bj-nnfim

Description: Nonfreeness in the antecedent and the consequent of an implication implies nonfreeness in the implication. (Contributed by BJ, 27-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		19.35	|- ( E. x ( ph -> ps ) <-> ( A. x ph -> E. x ps ) )
2		bj-nnfim2	|- ( ( F// x ph /\ F// x ps ) -> ( ( A. x ph -> E. x ps ) -> ( ph -> ps ) ) )
3	1 2	syl5bi	|- ( ( F// x ph /\ F// x ps ) -> ( E. x ( ph -> ps ) -> ( ph -> ps ) ) )
4		bj-nnfim1	|- ( ( F// x ph /\ F// x ps ) -> ( ( ph -> ps ) -> ( E. x ph -> A. x ps ) ) )
5		19.38	|- ( ( E. x ph -> A. x ps ) -> A. x ( ph -> ps ) )
6	4 5	syl6	|- ( ( F// x ph /\ F// x ps ) -> ( ( ph -> ps ) -> A. x ( ph -> ps ) ) )
7		df-bj-nnf	|- ( F// x ( ph -> ps ) <-> ( ( E. x ( ph -> ps ) -> ( ph -> ps ) ) /\ ( ( ph -> ps ) -> A. x ( ph -> ps ) ) ) )
8	3 6 7	sylanbrc	|- ( ( F// x ph /\ F// x ps ) -> F// x ( ph -> ps ) )