This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pm2.01i

Description: Inference associated with the weak Clavius law pm2.01 . (Contributed by BJ, 30-Mar-2020)

Ref Expression
Hypothesis pm2.01i.1 
|- ( ph -> -. ph )
Assertion pm2.01i 
|- -. ph

Proof

Step Hyp Ref Expression
1 pm2.01i.1 
 |-  ( ph -> -. ph )
2 pm2.01 
 |-  ( ( ph -> -. ph ) -> -. ph )
3 1 2 ax-mp 
 |-  -. ph