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 1792  ax-4 1806
This theorem depends on definitions:  df-bi 209  df-sb 2066
This theorem is referenced by:  sb2imi  2076  sbbii  2077  sban  2082  sb4av  2239  sbi2  2306  sbi2vOLD  2320  sbievOLD  2327  hbsb3  2522  sb6f  2533  sbie  2540  2mo  2729  fmptdF  30395  funcnv4mpt  30408  disjdsct  30432  measiuns  31471  ballotlemodife  31750  bj-hbsb3v  34132  bj-sbidmOLD  34169  mptsnunlem  34613  sbor2  39097
  Copyright terms: Public domain W3C validator