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

Theorem sbimi 2079
Description: Distribute substitution over implication. (Contributed by NM, 25-Jun-1998.) Revise df-sb 2068. (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 2071 . 2 [𝑡 / 𝑥](𝜑𝜓)
3 sbi1 2076 . 2 ([𝑡 / 𝑥](𝜑𝜓) → ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓))
42, 3ax-mp 5 1 ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  [wsb 2067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068
This theorem is referenced by:  sb2imi  2080  sbbii  2081  sban  2085  hbsbw  2176  sb4av  2251  sbi2  2308  hbsb3  2491  sb6f  2501  sbie  2506  2mo  2648  sbhypf  3502  elrabi  3642  fmptdF  32734  funcnv4mpt  32747  disjdsct  32782  measiuns  34374  ballotlemodife  34655  subsym1  36621  bj-hbsb3v  37016  bj-sbidmOLD  37051  mptsnunlem  37539  sbor2  42462
  Copyright terms: Public domain W3C validator