Metamath Proof Explorer

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	$⊢ (Ⅎ' x φ \land Ⅎ' x ψ) \to Ⅎ' x (φ \to ψ)$

Proof

Step	Hyp	Ref	Expression
1		19.35	$⊢ \exists x (φ \to ψ) \leftrightarrow (\forall x φ \to \exists x ψ)$
2		bj-nnfim2	$⊢ (Ⅎ' x φ \land Ⅎ' x ψ) \to ((\forall x φ \to \exists x ψ) \to (φ \to ψ))$
3	1 2	biimtrid	$⊢ (Ⅎ' x φ \land Ⅎ' x ψ) \to (\exists x (φ \to ψ) \to (φ \to ψ))$
4		bj-nnfim1	$⊢ (Ⅎ' x φ \land Ⅎ' x ψ) \to ((φ \to ψ) \to (\exists x φ \to \forall x ψ))$
5		19.38	$⊢ (\exists x φ \to \forall x ψ) \to \forall x (φ \to ψ)$
6	4 5	syl6	$⊢ (Ⅎ' x φ \land Ⅎ' x ψ) \to ((φ \to ψ) \to \forall x (φ \to ψ))$
7		df-bj-nnf	$⊢ Ⅎ' x (φ \to ψ) \leftrightarrow ((\exists x (φ \to ψ) \to (φ \to ψ)) \land ((φ \to ψ) \to \forall x (φ \to ψ)))$
8	3 6 7	sylanbrc	$⊢ (Ⅎ' x φ \land Ⅎ' x ψ) \to Ⅎ' x (φ \to ψ)$