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

Theorem sbimi 2073
Description: Distribute substitution over implication. (Contributed by NM, 25-Jun-1998.) Revise df-sb 2064. (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 2065 . 2 [𝑡 / 𝑥](𝜑𝜓)
3 sbi1 2070 . 2 ([𝑡 / 𝑥](𝜑𝜓) → ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓))
42, 3ax-mp 5 1 ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  [wsb 2063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808
This theorem depends on definitions:  df-bi 207  df-sb 2064
This theorem is referenced by:  sb2imi  2074  sbbii  2075  sban  2079  hbsbw  2170  sb4av  2243  sbi2  2301  hbsb3  2491  sb6f  2501  sbie  2506  2mo  2647  sbhypf  3543  elrabi  3686  fmptdF  32667  funcnv4mpt  32680  disjdsct  32713  measiuns  34219  ballotlemodife  34501  subsym1  36429  bj-hbsb3v  36817  bj-sbidmOLD  36852  mptsnunlem  37340  sbor2  42252
  Copyright terms: Public domain W3C validator