Metamath Proof Explorer

Theorem sbi1

Description: Distribute substitution over implication. (Contributed by NM, 14-May-1993) Remove dependencies on axioms. (Revised by Steven Nguyen, 24-Jul-2023)

		Ref	Expression
	Assertion	sbi1	$⊢ [y/ x] (φ \to ψ) \to ([y/ x] φ \to [y/ x] ψ)$

Proof

Step	Hyp	Ref	Expression
1		df-sb	$⊢ [y/ x] (φ \to ψ) \leftrightarrow \forall z (z = y \to \forall x (x = z \to (φ \to ψ)))$
2		ax-2	$⊢ (x = z \to (φ \to ψ)) \to ((x = z \to φ) \to (x = z \to ψ))$
3	2	al2imi	$⊢ \forall x (x = z \to (φ \to ψ)) \to (\forall x (x = z \to φ) \to \forall x (x = z \to ψ))$
4	3	imim3i	$⊢ (z = y \to \forall x (x = z \to (φ \to ψ))) \to ((z = y \to \forall x (x = z \to φ)) \to (z = y \to \forall x (x = z \to ψ)))$
5	4	al2imi	$⊢ \forall z (z = y \to \forall x (x = z \to (φ \to ψ))) \to (\forall z (z = y \to \forall x (x = z \to φ)) \to \forall z (z = y \to \forall x (x = z \to ψ)))$
6		df-sb	$⊢ [y/ x] φ \leftrightarrow \forall z (z = y \to \forall x (x = z \to φ))$
7		df-sb	$⊢ [y/ x] ψ \leftrightarrow \forall z (z = y \to \forall x (x = z \to ψ))$
8	5 6 7	3imtr4g	$⊢ \forall z (z = y \to \forall x (x = z \to (φ \to ψ))) \to ([y/ x] φ \to [y/ x] ψ)$
9	1 8	sylbi	$⊢ [y/ x] (φ \to ψ) \to ([y/ x] φ \to [y/ x] ψ)$