Theorem sb2imi

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

	Ref	Expression
Hypothesis	sb2imi.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
Assertion	sb2imi	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 → ( [ 𝑡 / 𝑥 ] 𝜓 → [ 𝑡 / 𝑥 ] 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		sb2imi.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2	1	sbimi	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 → [ 𝑡 / 𝑥 ] ( 𝜓 → 𝜒 ) )
3		sbi1	⊢ ( [ 𝑡 / 𝑥 ] ( 𝜓 → 𝜒 ) → ( [ 𝑡 / 𝑥 ] 𝜓 → [ 𝑡 / 𝑥 ] 𝜒 ) )
4	2 3	syl	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 → ( [ 𝑡 / 𝑥 ] 𝜓 → [ 𝑡 / 𝑥 ] 𝜒 ) )