Metamath Proof Explorer

Theorem pm2.24d

Description: Deduction form of pm2.24 . (Contributed by NM, 30-Jan-2006)

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

Proof

Step Hyp Ref Expression
1 pm2.24d.1 
 |-  ( ph -> ps )
2 1 a1d 
 |-  ( ph -> ( -. ch -> ps ) )
3 2 con1d 
 |-  ( ph -> ( -. ps -> ch ) )