Theorem sbimi 2079

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

Syntax hints:   → wi 4  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068

This theorem is referenced by:  sb2imi  2080  sbbii  2081  sban  2085  hbsbw  2176  sb4av  2249  sbi2  2306  hbsb3  2489  sb6f  2499  sbie  2504  2mo  2645  sbhypf  3499  elrabi  3639  fmptdF  32640  funcnv4mpt  32653  disjdsct  32688  measiuns  34251  ballotlemodife  34532  subsym1  36492  bj-hbsb3v  36880  bj-sbidmOLD  36915  mptsnunlem  37403  sbor2  42326