Theorem sbimi 2080

Description: Distribute substitution over implication. (Contributed by NM, 25-Jun-1998.) Revise df-sb 2071. (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 2070

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

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

This theorem is referenced by:  sb2imi  2081  sbbii  2082  sban  2086  sb4av  2239  sbi2  2302  hbsb3  2492  sb6f  2502  sbie  2507  2mo  2651  elrabi  3619  fmptdF  30972  funcnv4mpt  30985  disjdsct  31014  measiuns  32164  ballotlemodife  32443  bj-hbsb3v  34976  bj-sbidmOLD  35013  mptsnunlem  35488  sbor2  40157