Theorem sbimi 2075

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

Syntax hints:   → wi 4  [wsb 2065

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

This theorem depends on definitions:  df-bi 207  df-sb 2066

This theorem is referenced by:  sb2imi  2076  sbbii  2077  sban  2081  hbsbw  2172  sb4av  2245  sbi2  2302  hbsb3  2486  sb6f  2496  sbie  2501  2mo  2642  sbhypf  3513  elrabi  3657  fmptdF  32587  funcnv4mpt  32600  disjdsct  32633  measiuns  34214  ballotlemodife  34496  subsym1  36422  bj-hbsb3v  36810  bj-sbidmOLD  36845  mptsnunlem  37333  sbor2  42207