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

Theorem sbimi 2075
Description: Distribute substitution over implication. (Contributed by NM, 25-Jun-1998.) Revise df-sb 2066. (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 2067 . 2 [𝑡 / 𝑥](𝜑𝜓)
3 sbi1 2072 . 2 ([𝑡 / 𝑥](𝜑𝜓) → ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓))
42, 3ax-mp 5 1 ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  [wsb 2065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-sb 2066
This theorem is referenced by:  sb2imi  2076  sbbii  2077  sban  2081  hbsbw  2172  sb4av  2245  sbi2  2302  hbsb3  2485  sb6f  2495  sbie  2500  2mo  2641  sbhypf  3499  elrabi  3643  fmptdF  32600  funcnv4mpt  32613  disjdsct  32646  measiuns  34190  ballotlemodife  34472  subsym1  36411  bj-hbsb3v  36799  bj-sbidmOLD  36834  mptsnunlem  37322  sbor2  42195
  Copyright terms: Public domain W3C validator