Metamath Proof Explorer

Theorem pm2.21d

Description: A contradiction implies anything. Deduction associated with pm2.21 . (Contributed by NM, 10-Feb-1996)

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

Proof

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