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  2280  sbi2  2336  hbsb3  2517  sb6f  2527  sbie  2532  2mo  2674  sbhypf  3510  elrabi  3641  fmptdf2  33232  funcnv4mpt  33244  disjdsct  33278  measiuns  34832  ballotlemodife  35113  subsym1  37185  bj-hbsb3v  37697  bj-sbidmOLD  37732  mptsnunlem  38229  sbor2  43232