Description: Inference associated with the weak Clavius law pm2.01 . (Contributed by BJ, 30-Mar-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | bj-pm2.01i.1 | |- ( ph -> -. ph ) |
|
Assertion | bj-pm2.01i | |- -. ph |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-pm2.01i.1 | |- ( ph -> -. ph ) |
|
2 | pm2.01 | |- ( ( ph -> -. ph ) -> -. ph ) |
|
3 | 1 2 | ax-mp | |- -. ph |