Theorem sbimi 2069

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

Syntax hints:   → wi 4  [wsb 2059

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

This theorem depends on definitions:  df-bi 206  df-sb 2060

This theorem is referenced by:  sb2imi  2070  sbbii  2071  sban  2075  hbsbw  2160  sb4av  2231  sbi2  2291  hbsb3  2481  sb6f  2491  sbie  2496  2mo  2639  sbhypf  3536  elrabi  3676  fmptdF  32460  funcnv4mpt  32473  disjdsct  32500  measiuns  33841  ballotlemodife  34122  subsym1  35916  bj-hbsb3v  36297  bj-sbidmOLD  36332  mptsnunlem  36822  sbor2  41703