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 1792  ax-4 1806

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

This theorem is referenced by:  sb2imi  2076  sbbii  2077  sban  2082  sb4av  2240  sbi2  2306  sbi2vOLD  2320  sbievOLD  2327  hbsb3  2522  sb6f  2533  sbie  2540  2mo  2729  fmptdF  30395  funcnv4mpt  30408  disjdsct  30432  measiuns  31471  ballotlemodife  31750  bj-hbsb3v  34132  bj-sbidmOLD  34169  mptsnunlem  34613  sbor2  39097