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

Proof

Step	Hyp	Ref	Expression
1		19.35	⊢ ( ∃ 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) )
2		bj-nnfim2	⊢ ( ( Ⅎ' 𝑥 𝜑 ∧ Ⅎ' 𝑥 𝜓 ) → ( ( ∀ 𝑥 𝜑 → ∃ 𝑥 𝜓 ) → ( 𝜑 → 𝜓 ) ) )
3	1 2	syl5bi	⊢ ( ( Ⅎ' 𝑥 𝜑 ∧ Ⅎ' 𝑥 𝜓 ) → ( ∃ 𝑥 ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) )
4		bj-nnfim1	⊢ ( ( Ⅎ' 𝑥 𝜑 ∧ Ⅎ' 𝑥 𝜓 ) → ( ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) ) )
5		19.38	⊢ ( ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) → ∀ 𝑥 ( 𝜑 → 𝜓 ) )
6	4 5	syl6	⊢ ( ( Ⅎ' 𝑥 𝜑 ∧ Ⅎ' 𝑥 𝜓 ) → ( ( 𝜑 → 𝜓 ) → ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )
7		df-bj-nnf	⊢ ( Ⅎ' 𝑥 ( 𝜑 → 𝜓 ) ↔ ( ( ∃ 𝑥 ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) ∧ ( ( 𝜑 → 𝜓 ) → ∀ 𝑥 ( 𝜑 → 𝜓 ) ) ) )
8	3 6 7	sylanbrc	⊢ ( ( Ⅎ' 𝑥 𝜑 ∧ Ⅎ' 𝑥 𝜓 ) → Ⅎ' 𝑥 ( 𝜑 → 𝜓 ) )