Theorem sbimi 2084

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

Syntax hints:   → wi 4  [wsb 2074

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

This theorem depends on definitions:  df-bi 210  df-sb 2075

This theorem is referenced by:  sb2imi  2085  sbbii  2086  sban  2090  sb4av  2245  sbi2  2306  hbsb3  2491  sb6f  2501  sbie  2506  2mo  2651  elrabi  3582  fmptdF  30568  funcnv4mpt  30581  disjdsct  30610  measiuns  31755  ballotlemodife  32034  bj-hbsb3v  34628  bj-sbidmOLD  34665  mptsnunlem  35132  sbor2  39768