Theorem sbimi

Description: Distribute substitution over implication. (Contributed by NM, 25-Jun-1998) Revise df-sb . (Revised by BJ, 22-Dec-2020) (Proof shortened by Steven Nguyen, 24-Jul-2023)

	Ref	Expression
Hypothesis	sbimi.1	$$⊢\phi \to \psi$$
Assertion	sbimi	$$⊢\left[t/x\right]\phi \to \left[t/x\right]\psi$$

Proof

Step	Hyp	Ref	Expression
1		sbimi.1	$$⊢\phi \to \psi$$
2	1	sbt	$$⊢\left[t/x\right]\left(\phi \to \psi \right)$$
3		sbi1	$$⊢\left[t/x\right]\left(\phi \to \psi \right)\to \left(\left[t/x\right]\phi \to \left[t/x\right]\psi \right)$$
4	2 3	ax-mp	$$⊢\left[t/x\right]\phi \to \left[t/x\right]\psi$$