Theorem sbimi 2077

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 2069	. 2 ⊢ [𝑡 / 𝑥](𝜑 → 𝜓)
3		sbi1 2074	. 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

This theorem depends on definitions:  df-bi 207  df-sb 2068

This theorem is referenced by:  sb2imi  2078  sbbii  2079  sban  2083  hbsbw  2174  sb4av  2247  sbi2  2304  hbsb3  2487  sb6f  2497  sbie  2502  2mo  2643  sbhypf  3499  elrabi  3643  fmptdF  32636  funcnv4mpt  32649  disjdsct  32682  measiuns  34228  ballotlemodife  34509  subsym1  36467  bj-hbsb3v  36855  bj-sbidmOLD  36890  mptsnunlem  37378  sbor2  42251