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  33038  funcnv4mpt  33050  disjdsct  33085  measiuns  34639  ballotlemodife  34920  subsym1  36979  bj-hbsb3v  37491  bj-sbidmOLD  37526  mptsnunlem  38025  sbor2  43022