Theorem sbimi 2113

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

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

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 1945  ax-6 2002  ax-7 2043

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

This theorem is used by:  sb2imi  2114  sbbii  2115  sban  2119  sbrimvw  2130  hbsbw  2211  sb4av  2283  sbi2  2339  hbsb3  2519  sb6f  2529  sbie  2534  2mo  2676  sbhypf  3513  elrabi  3644  fmptdf2  33322  funcnv4mpt  33334  disjdsct  33367  measiuns  34920  ballotlemodife  35200  subsym1  37393  bj-hbsb3v  37905  bj-sbidmOLD  37940  mptsnunlem  38453  sbor2  43457