Metamath Proof Explorer

Theorem pm2.18i

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

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

Proof

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