Theorem sbimi 2108

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

Syntax hints:   → wi 4  [wsb 2096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097

This theorem is referenced by:  sb2imi  2109  sbbii  2110  sban  2114  sbrimvw  2125  hbsbw  2206  sb4av  2280  sbi2  2337  hbsb3  2519  sb6f  2529  sbie  2534  2mo  2676  sbhypf  3514  elrabi  3647  fmptdF  32979  funcnv4mpt  32991  disjdsct  33026  measiuns  34585  ballotlemodife  34866  subsym1  36916  bj-hbsb3v  37428  bj-sbidmOLD  37463  mptsnunlem  37962  sbor2  42959