Theorem sbimi 2110

Description: Distribute substitution over implication. (Contributed by NM, 25-Jun-1998.) Revise df-sb 2099. (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 2102	. 2 ⊢ [𝑡 / 𝑥](𝜑 → 𝜓)
3		sbi1 2107	. 2 ⊢ ([𝑡 / 𝑥](𝜑 → 𝜓) → ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓))
4	2, 3	ax-mp 5	1 ⊢ ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)

This proof depends on syntax axioms:   → wi 4  [wsb 2098

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099

This theorem is used by:  sb2imi  2111  sbbii  2112  sban  2116  sbrimvw  2127  hbsbw  2207  sb4av  2279  sbi2  2335  hbsb3  2516  sb6f  2526  sbie  2531  2mo  2673  sbhypf  3509  elrabi  3640  fmptdf2  33297  funcnv4mpt  33309  disjdsct  33343  measiuns  34896  ballotlemodife  35176  subsym1  37307  bj-hbsb3v  37819  bj-sbidmOLD  37854  mptsnunlem  38354  sbor2  43357