Description: Alternate proof of sbn1 , not using the false constant. (Contributed by BJ, 18-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sbn1ALT | |- ( [ t / x ] -. ph -> -. [ t / x ] ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nsb | |- ( A. x -. ( ph /\ -. ph ) -> -. [ t / x ] ( ph /\ -. ph ) ) |
|
| 2 | pm3.24 | |- -. ( ph /\ -. ph ) |
|
| 3 | 1 2 | mpg | |- -. [ t / x ] ( ph /\ -. ph ) |
| 4 | sban | |- ( [ t / x ] ( ph /\ -. ph ) <-> ( [ t / x ] ph /\ [ t / x ] -. ph ) ) |
|
| 5 | 3 4 | mtbi | |- -. ( [ t / x ] ph /\ [ t / x ] -. ph ) |
| 6 | pm3.21 | |- ( [ t / x ] -. ph -> ( [ t / x ] ph -> ( [ t / x ] ph /\ [ t / x ] -. ph ) ) ) |
|
| 7 | 5 6 | mtoi | |- ( [ t / x ] -. ph -> -. [ t / x ] ph ) |