sbi1lem

Description: Lemma for sbi1 . The core of the proof was extracted from a proof of SN. (Contributed by Wolf Lammen, 5-Jun-2026)

		Ref	Expression
	Assertion	sbi1lem	$⊢ ([t/ x] (φ \to ψ) \land [t/ x] φ) \to \forall y (y = t \to \forall x (x = y \to ψ))$

Step	Hyp	Ref	Expression
1		dfsbimp	$⊢ [t/ x] (φ \to ψ) \to \forall y (y = t \to \forall x (x = y \to (φ \to ψ)))$
2		dfsbimp	$⊢ [t/ x] φ \to \forall y (y = t \to \forall x (x = y \to φ))$
3		ax-2	$⊢ (x = y \to (φ \to ψ)) \to ((x = y \to φ) \to (x = y \to ψ))$
4	3	al2imi	$⊢ \forall x (x = y \to (φ \to ψ)) \to (\forall x (x = y \to φ) \to \forall x (x = y \to ψ))$
5	4	imim3i	$⊢ (y = t \to \forall x (x = y \to (φ \to ψ))) \to ((y = t \to \forall x (x = y \to φ)) \to (y = t \to \forall x (x = y \to ψ)))$
6	5	al2imi	$⊢ \forall y (y = t \to \forall x (x = y \to (φ \to ψ))) \to (\forall y (y = t \to \forall x (x = y \to φ)) \to \forall y (y = t \to \forall x (x = y \to ψ)))$
7	1 2 6	syl2im	$⊢ [t/ x] (φ \to ψ) \to ([t/ x] φ \to \forall y (y = t \to \forall x (x = y \to ψ)))$
8	7	imp	$⊢ ([t/ x] (φ \to ψ) \land [t/ x] φ) \to \forall y (y = t \to \forall x (x = y \to ψ))$

Metamath Proof Explorer