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