Theorem sbimi 2078

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

Syntax hints:   → wi 4  [wsb 2068

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

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

This theorem is referenced by:  sb2imi  2079  sbbii  2080  sban  2084  sb4av  2237  sbi2  2299  hbsb3  2487  sb6f  2497  sbie  2502  2mo  2645  sbhypf  3539  elrabi  3677  fmptdF  31869  funcnv4mpt  31882  disjdsct  31912  measiuns  33204  ballotlemodife  33485  subsym1  35301  bj-hbsb3v  35682  bj-sbidmOLD  35718  mptsnunlem  36208  sbor2  41024