Theorem sbimi 2106

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

Syntax hints:   → wi 4  [wsb 2089

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-sb 2090

This theorem is referenced by:  sb2imi  2107  sbbii  2108  sban  2112  sbrimvw  2123  hbsbw  2204  sb4av  2278  sbi2  2335  hbsb3  2517  sb6f  2527  sbie  2532  2mo  2674  sbhypf  3512  elrabi  3646  fmptdF  32808  funcnv4mpt  32820  disjdsct  32855  measiuns  34475  ballotlemodife  34756  subsym1  36751  bj-hbsb3v  37264  bj-sbidmOLD  37299  mptsnunlem  37796  sbor2  42793