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	⊢ ( 𝜑 → Ⅎ' 𝑥 𝜓 )
	bj-nnfbid.2	⊢ ( 𝜑 → Ⅎ' 𝑥 𝜒 )
Assertion	bj-nnfbid	⊢ ( 𝜑 → Ⅎ' 𝑥 ( 𝜓 ↔ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-nnfbid.1	⊢ ( 𝜑 → Ⅎ' 𝑥 𝜓 )
2		bj-nnfbid.2	⊢ ( 𝜑 → Ⅎ' 𝑥 𝜒 )
3		bj-nnfim	⊢ ( ( Ⅎ' 𝑥 𝜓 ∧ Ⅎ' 𝑥 𝜒 ) → Ⅎ' 𝑥 ( 𝜓 → 𝜒 ) )
4	1 2 3	syl2anc	⊢ ( 𝜑 → Ⅎ' 𝑥 ( 𝜓 → 𝜒 ) )
5		bj-nnfim	⊢ ( ( Ⅎ' 𝑥 𝜒 ∧ Ⅎ' 𝑥 𝜓 ) → Ⅎ' 𝑥 ( 𝜒 → 𝜓 ) )
6	2 1 5	syl2anc	⊢ ( 𝜑 → Ⅎ' 𝑥 ( 𝜒 → 𝜓 ) )
7	4 6	bj-nnfand	⊢ ( 𝜑 → Ⅎ' 𝑥 ( ( 𝜓 → 𝜒 ) ∧ ( 𝜒 → 𝜓 ) ) )
8		dfbi2	⊢ ( ( 𝜓 ↔ 𝜒 ) ↔ ( ( 𝜓 → 𝜒 ) ∧ ( 𝜒 → 𝜓 ) ) )
9	8	bj-nnfbii	⊢ ( Ⅎ' 𝑥 ( 𝜓 ↔ 𝜒 ) ↔ Ⅎ' 𝑥 ( ( 𝜓 → 𝜒 ) ∧ ( 𝜒 → 𝜓 ) ) )
10	7 9	sylibr	⊢ ( 𝜑 → Ⅎ' 𝑥 ( 𝜓 ↔ 𝜒 ) )