Theorem sbimi 2072

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

Syntax hints:   → wi 4  [wsb 2062

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 207  df-sb 2063

This theorem is referenced by:  sb2imi  2073  sbbii  2074  sban  2078  hbsbw  2169  sb4av  2242  sbi2  2301  hbsb3  2490  sb6f  2500  sbie  2505  2mo  2646  sbhypf  3544  elrabi  3690  fmptdF  32673  funcnv4mpt  32686  disjdsct  32718  measiuns  34198  ballotlemodife  34479  subsym1  36410  bj-hbsb3v  36798  bj-sbidmOLD  36833  mptsnunlem  37321  sbor2  42230