Theorem sbimi 2075

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

Syntax hints:   → wi 4  [wsb 2065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809

This theorem depends on definitions:  df-bi 206  df-sb 2066

This theorem is referenced by:  sb2imi  2076  sbbii  2077  sban  2081  sb4av  2234  sbi2  2296  hbsb3  2484  sb6f  2494  sbie  2499  2mo  2642  sbhypf  3537  elrabi  3678  fmptdF  32146  funcnv4mpt  32159  disjdsct  32189  measiuns  33511  ballotlemodife  33792  subsym1  35617  bj-hbsb3v  35998  bj-sbidmOLD  36034  mptsnunlem  36524  sbor2  41336