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  3678  fmptdF  31881  funcnv4mpt  31894  disjdsct  31924  measiuns  33215  ballotlemodife  33496  subsym1  35312  bj-hbsb3v  35693  bj-sbidmOLD  35729  mptsnunlem  36219  sbor2  41028