|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > sbimi | Structured version Visualization version GIF version | ||
| 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.) | 
| Ref | Expression | 
|---|---|
| sbimi.1 | ⊢ (𝜑 → 𝜓) | 
| Ref | Expression | 
|---|---|
| sbimi | ⊢ ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | sbimi.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
| 2 | 1 | sbt 2065 | . 2 ⊢ [𝑡 / 𝑥](𝜑 → 𝜓) | 
| 3 | sbi1 2070 | . 2 ⊢ ([𝑡 / 𝑥](𝜑 → 𝜓) → ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)) | |
| 4 | 2, 3 | ax-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 |