Theorem bj-nnfbit

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

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

Proof

Step	Hyp	Ref	Expression
1		bj-nnfim	|- ( ( F// x ph /\ F// x ps ) -> F// x ( ph -> ps ) )
2		bj-nnfim	|- ( ( F// x ps /\ F// x ph ) -> F// x ( ps -> ph ) )
3	2	ancoms	|- ( ( F// x ph /\ F// x ps ) -> F// x ( ps -> ph ) )
4		bj-nnfan	|- ( ( F// x ( ph -> ps ) /\ F// x ( ps -> ph ) ) -> F// x ( ( ph -> ps ) /\ ( ps -> ph ) ) )
5	1 3 4	syl2anc	|- ( ( F// x ph /\ F// x ps ) -> F// x ( ( ph -> ps ) /\ ( ps -> ph ) ) )
6		dfbi2	|- ( ( ph <-> ps ) <-> ( ( ph -> ps ) /\ ( ps -> ph ) ) )
7	6	bicomi	|- ( ( ( ph -> ps ) /\ ( ps -> ph ) ) <-> ( ph <-> ps ) )
8	7	bj-nnfbii	|- ( F// x ( ( ph -> ps ) /\ ( ps -> ph ) ) <-> F// x ( ph <-> ps ) )
9	5 8	sylib	|- ( ( F// x ph /\ F// x ps ) -> F// x ( ph <-> ps ) )