Theorem sbimi 2080

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 2072	. 2 ⊢ [𝑡 / 𝑥](𝜑 → 𝜓)
3		sbi1 2077	. 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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069

This theorem is referenced by:  sb2imi  2081  sbbii  2082  sban  2086  hbsbw  2177  sb4av  2252  sbi2  2309  hbsb3  2491  sb6f  2501  sbie  2506  2mo  2648  sbhypf  3490  elrabi  3630  fmptdF  32729  funcnv4mpt  32741  disjdsct  32776  measiuns  34361  ballotlemodife  34642  subsym1  36609  bj-hbsb3v  37122  bj-sbidmOLD  37157  mptsnunlem  37654  sbor2  42651