Theorem sbimi 2111

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100

This theorem is used by:  sb2imi  2112  sbbii  2113  sban  2117  sbrimvw  2128  hbsbw  2208  sb4av  2281  sbi2  2337  hbsb3  2518  sb6f  2528  sbie  2533  2mo  2675  sbhypf  3512  elrabi  3644  fmptdf2  33137  funcnv4mpt  33149  disjdsct  33183  measiuns  34736  ballotlemodife  35017  subsym1  37054  bj-hbsb3v  37566  bj-sbidmOLD  37601  mptsnunlem  38100  sbor2  43088