Theorem sbimi 2080

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069

This theorem is referenced by:  sb2imi  2081  sbbii  2082  sban  2086  hbsbw  2177  sb4av  2252  sbi2  2309  hbsb3  2492  sb6f  2502  sbie  2507  2mo  2649  sbhypf  3491  elrabi  3631  fmptdF  32744  funcnv4mpt  32756  disjdsct  32791  measiuns  34377  ballotlemodife  34658  subsym1  36625  bj-hbsb3v  37138  bj-sbidmOLD  37173  mptsnunlem  37668  sbor2  42665