![]() |
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 2060. (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 2061 | . 2 ⊢ [𝑡 / 𝑥](𝜑 → 𝜓) |
3 | sbi1 2066 | . 2 ⊢ ([𝑡 / 𝑥](𝜑 → 𝜓) → ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)) | |
4 | 2, 3 | ax-mp 5 | 1 ⊢ ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 [wsb 2059 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 |
This theorem depends on definitions: df-bi 206 df-sb 2060 |
This theorem is referenced by: sb2imi 2070 sbbii 2071 sban 2075 hbsbw 2160 sb4av 2231 sbi2 2291 hbsb3 2481 sb6f 2491 sbie 2496 2mo 2639 sbhypf 3536 elrabi 3676 fmptdF 32460 funcnv4mpt 32473 disjdsct 32500 measiuns 33841 ballotlemodife 34122 subsym1 35916 bj-hbsb3v 36297 bj-sbidmOLD 36332 mptsnunlem 36822 sbor2 41703 |
Copyright terms: Public domain | W3C validator |