Metamath Proof Explorer

Theorem mtod

Description: Modus tollens deduction. (Contributed by NM, 3-Apr-1994) (Proof shortened by Wolf Lammen, 11-Sep-2013)

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

Proof

Step Hyp Ref Expression
1 mtod.1 
 |-  ( ph -> -. ch )
2 mtod.2 
 |-  ( ph -> ( ps -> ch ) )
3 1 a1d 
 |-  ( ph -> ( ps -> -. ch ) )
4 2 3 pm2.65d 
 |-  ( ph -> -. ps )