Metamath Proof Explorer

Theorem pm2.24i

Description: Inference associated with pm2.24 . Its associated inference is pm2.24ii . (Contributed by NM, 20-Aug-2001)

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

Proof

Step Hyp Ref Expression
1 pm2.24i.1 
 |-  ph
2 1 a1i 
 |-  ( -. ps -> ph )
3 2 con1i 
 |-  ( -. ph -> ps )