Theorem sbimi 2085

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

Syntax hints:   → wi 4  [wsb 2073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074

This theorem is referenced by:  sb2imi  2086  sbbii  2087  sban  2091  hbsbw  2182  sb4av  2256  sbi2  2313  hbsb3  2495  sb6f  2505  sbie  2510  2mo  2652  sbhypf  3493  elrabi  3632  fmptdF  32755  funcnv4mpt  32767  disjdsct  32802  measiuns  34408  ballotlemodife  34689  subsym1  36662  bj-hbsb3v  37175  bj-sbidmOLD  37210  mptsnunlem  37707  sbor2  42704