Metamath Proof Explorer

Theorem mtand

Description: A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009)

Ref Expression
Hypotheses mtand.1 
|- ( ph -> -. ch )
mtand.2 
|- ( ( ph /\ ps ) -> ch )
Assertion mtand 
|- ( ph -> -. ps )

Proof

Step Hyp Ref Expression
1 mtand.1 
 |-  ( ph -> -. ch )
2 mtand.2 
 |-  ( ( ph /\ ps ) -> ch )
3 2 ex 
 |-  ( ph -> ( ps -> ch ) )
4 1 3 mtod 
 |-  ( ph -> -. ps )