Theorem bj-nnfbid

Description: Nonfreeness in both sides implies nonfreeness in the biconditional, deduction form. (Contributed by BJ, 2-Dec-2023) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bj-nnfbid.1	|- ( ph -> F// x ps )
	bj-nnfbid.2	|- ( ph -> F// x ch )
Assertion	bj-nnfbid	|- ( ph -> F// x ( ps <-> ch ) )

Proof

Step	Hyp	Ref	Expression
1		bj-nnfbid.1	|- ( ph -> F// x ps )
2		bj-nnfbid.2	|- ( ph -> F// x ch )
3		bj-nnfim	|- ( ( F// x ps /\ F// x ch ) -> F// x ( ps -> ch ) )
4	1 2 3	syl2anc	|- ( ph -> F// x ( ps -> ch ) )
5		bj-nnfim	|- ( ( F// x ch /\ F// x ps ) -> F// x ( ch -> ps ) )
6	2 1 5	syl2anc	|- ( ph -> F// x ( ch -> ps ) )
7	4 6	bj-nnfand	|- ( ph -> F// x ( ( ps -> ch ) /\ ( ch -> ps ) ) )
8		dfbi2	|- ( ( ps <-> ch ) <-> ( ( ps -> ch ) /\ ( ch -> ps ) ) )
9	8	bj-nnfbii	|- ( F// x ( ps <-> ch ) <-> F// x ( ( ps -> ch ) /\ ( ch -> ps ) ) )
10	7 9	sylibr	|- ( ph -> F// x ( ps <-> ch ) )