Metamath Proof Explorer

Theorem mt4d

Description: Modus tollens deduction. Deduction form of mt4 . (Contributed by NM, 9-Jun-2006)

Ref Expression
Hypotheses mt4d.1 
|- ( ph -> ps )
mt4d.2 
|- ( ph -> ( -. ch -> -. ps ) )
Assertion mt4d 
|- ( ph -> ch )

Proof

Step Hyp Ref Expression
1 mt4d.1 
 |-  ( ph -> ps )
2 mt4d.2 
 |-  ( ph -> ( -. ch -> -. ps ) )
3 2 con4d 
 |-  ( ph -> ( ps -> ch ) )
4 1 3 mpd 
 |-  ( ph -> ch )