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 ) )