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 2066. (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 2067 | . 2 ⊢ [𝑡 / 𝑥](𝜑 → 𝜓) |
3 | sbi1 2072 | . 2 ⊢ ([𝑡 / 𝑥](𝜑 → 𝜓) → ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)) | |
4 | 2, 3 | ax-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 2240 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 |