Theorem sb2imi

Description: Distribute substitution over implication. Compare al2imi . (Contributed by Steven Nguyen, 13-Aug-2023)

	Ref	Expression
Hypothesis	sb2imi.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
Assertion	sb2imi	$$⊢\left[t/x\right]\phi \to \left(\left[t/x\right]\psi \to \left[t/x\right]\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sb2imi.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
2	1	sbimi	$$⊢\left[t/x\right]\phi \to \left[t/x\right]\left(\psi \to \chi \right)$$
3		sbi1	$$⊢\left[t/x\right]\left(\psi \to \chi \right)\to \left(\left[t/x\right]\psi \to \left[t/x\right]\chi \right)$$
4	2 3	syl	$$⊢\left[t/x\right]\phi \to \left(\left[t/x\right]\psi \to \left[t/x\right]\chi \right)$$