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	⊢ ( ( Ⅎ' 𝑥 𝜑 ∧ Ⅎ' 𝑥 𝜓 ) → Ⅎ' 𝑥 ( 𝜑 ↔ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-nnfim	⊢ ( ( Ⅎ' 𝑥 𝜑 ∧ Ⅎ' 𝑥 𝜓 ) → Ⅎ' 𝑥 ( 𝜑 → 𝜓 ) )
2		bj-nnfim	⊢ ( ( Ⅎ' 𝑥 𝜓 ∧ Ⅎ' 𝑥 𝜑 ) → Ⅎ' 𝑥 ( 𝜓 → 𝜑 ) )
3	2	ancoms	⊢ ( ( Ⅎ' 𝑥 𝜑 ∧ Ⅎ' 𝑥 𝜓 ) → Ⅎ' 𝑥 ( 𝜓 → 𝜑 ) )
4		bj-nnfan	⊢ ( ( Ⅎ' 𝑥 ( 𝜑 → 𝜓 ) ∧ Ⅎ' 𝑥 ( 𝜓 → 𝜑 ) ) → Ⅎ' 𝑥 ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜑 ) ) )
5	1 3 4	syl2anc	⊢ ( ( Ⅎ' 𝑥 𝜑 ∧ Ⅎ' 𝑥 𝜓 ) → Ⅎ' 𝑥 ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜑 ) ) )
6		dfbi2	⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜑 ) ) )
7	6	bicomi	⊢ ( ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜑 ) ) ↔ ( 𝜑 ↔ 𝜓 ) )
8	7	bj-nnfbii	⊢ ( Ⅎ' 𝑥 ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜑 ) ) ↔ Ⅎ' 𝑥 ( 𝜑 ↔ 𝜓 ) )
9	5 8	sylib	⊢ ( ( Ⅎ' 𝑥 𝜑 ∧ Ⅎ' 𝑥 𝜓 ) → Ⅎ' 𝑥 ( 𝜑 ↔ 𝜓 ) )