Theorem sbimi 2110

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

Hypothesis

Ref	Expression
sbimi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
sbimi	⊢ ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)

Proof of Theorem sbimi

Step	Hyp	Ref	Expression
1		sbimi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	sbt 2098	. 2 ⊢ [𝑡 / 𝑥](𝜑 → 𝜓)
3		sbi1 2106	. 2 ⊢ ([𝑡 / 𝑥](𝜑 → 𝜓) → ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓))
4	2, 3	ax-mp 5	1 ⊢ ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)

Syntax hints:   → wi 4  [wsb 2093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832

This theorem depends on definitions:  df-bi 210  df-an 401  df-sb 2094

This theorem is referenced by:  sb2imi  2111  sbbii  2112  sban  2116  sbrimvw  2127  hbsbw  2208  sb4av  2282  sbi2  2339  hbsb3  2521  sb6f  2531  sbie  2536  2mo  2678  sbhypf  3516  elrabi  3649  fmptdF  32913  funcnv4mpt  32925  disjdsct  32960  measiuns  34524  ballotlemodife  34805  subsym1  36800  bj-hbsb3v  37312  bj-sbidmOLD  37347  mptsnunlem  37844  sbor2  42841