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  2209  sb4av  2283  sbi2  2340  hbsb3  2522  sb6f  2532  sbie  2537  2mo  2679  sbhypf  3517  elrabi  3649  fmptdf2  33016  funcnv4mpt  33028  disjdsct  33063  measiuns  34620  ballotlemodife  34901  subsym1  36970  bj-hbsb3v  37482  bj-sbidmOLD  37517  mptsnunlem  38016  sbor2  43013