MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbimi Structured version   Visualization version   GIF version

Theorem sbimi 2069
Description: Distribute substitution over implication. (Contributed by NM, 25-Jun-1998.) Revise df-sb 2060. (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
StepHypRef Expression
1 sbimi.1 . . 3 (𝜑𝜓)
21sbt 2061 . 2 [𝑡 / 𝑥](𝜑𝜓)
3 sbi1 2066 . 2 ([𝑡 / 𝑥](𝜑𝜓) → ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓))
42, 3ax-mp 5 1 ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  [wsb 2059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 206  df-sb 2060
This theorem is referenced by:  sb2imi  2070  sbbii  2071  sban  2075  hbsbw  2160  sb4av  2231  sbi2  2291  hbsb3  2481  sb6f  2491  sbie  2496  2mo  2639  sbhypf  3536  elrabi  3676  fmptdF  32460  funcnv4mpt  32473  disjdsct  32500  measiuns  33841  ballotlemodife  34122  subsym1  35916  bj-hbsb3v  36297  bj-sbidmOLD  36332  mptsnunlem  36822  sbor2  41703
  Copyright terms: Public domain W3C validator