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  2492  sb6f  2502  sbie  2507  2mo  2649  sbhypf  3504  elrabi  3644  fmptdF  32745  funcnv4mpt  32757  disjdsct  32792  measiuns  34394  ballotlemodife  34675  subsym1  36640  bj-hbsb3v  37057  bj-sbidmOLD  37092  mptsnunlem  37587  sbor2  42576