Description: Distribute substitution over implication. (Contributed by NM, 25-Jun-1998) Revise df-sb . (Revised by BJ, 22-Dec-2020) (Proof shortened by Steven Nguyen, 24-Jul-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | sbimi.1 | |- ( ph -> ps ) |
|
| Assertion | sbimi | |- ( [ t / x ] ph -> [ t / x ] ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbimi.1 | |- ( ph -> ps ) |
|
| 2 | 1 | sbt | |- [ t / x ] ( ph -> ps ) |
| 3 | sbi1 | |- ( [ t / x ] ( ph -> ps ) -> ( [ t / x ] ph -> [ t / x ] ps ) ) |
|
| 4 | 2 3 | ax-mp | |- ( [ t / x ] ph -> [ t / x ] ps ) |