bj-nnfim1

Description: A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023)

		Ref	Expression
	Assertion	bj-nnfim1	$⊢ (Ⅎ' x φ \land Ⅎ' x ψ) \to ((φ \to ψ) \to (\exists x φ \to \forall x ψ))$

Step	Hyp	Ref	Expression
1		bj-nnfe	$⊢ Ⅎ' x φ \to (\exists x φ \to φ)$
2		bj-nnfa	$⊢ Ⅎ' x ψ \to (ψ \to \forall x ψ)$
3		imim12	$⊢ (\exists x φ \to φ) \to ((ψ \to \forall x ψ) \to ((φ \to ψ) \to (\exists x φ \to \forall x ψ)))$
4	3	imp	$⊢ ((\exists x φ \to φ) \land (ψ \to \forall x ψ)) \to ((φ \to ψ) \to (\exists x φ \to \forall x ψ))$
5	1 2 4	syl2an	$⊢ (Ⅎ' x φ \land Ⅎ' x ψ) \to ((φ \to ψ) \to (\exists x φ \to \forall x ψ))$

Metamath Proof Explorer