Theorem sbimi 2074

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

Syntax hints:   → wi 4  [wsb 2064

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

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

This theorem is referenced by:  sb2imi  2075  sbbii  2076  sban  2080  hbsbw  2172  sb4av  2245  sbi2  2306  hbsb3  2495  sb6f  2505  sbie  2510  2mo  2651  sbhypf  3556  elrabi  3703  fmptdF  32674  funcnv4mpt  32687  disjdsct  32714  measiuns  34181  ballotlemodife  34462  subsym1  36393  bj-hbsb3v  36781  bj-sbidmOLD  36816  mptsnunlem  37304  sbor2  42205