MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mt4d Unicode version

Theorem mt4d 130
Description: Modus tollens deduction. (Contributed by NM, 9-Jun-2006.)
Hypotheses
Ref Expression
mt4d.1  |-  ( ph  ->  ps )
mt4d.2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
Assertion
Ref Expression
mt4d  |-  ( ph  ->  ch )

Proof of Theorem mt4d
StepHypRef Expression
1 mt4d.1 . 2  |-  ( ph  ->  ps )
2 mt4d.2 . . 3  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
32con4d 97 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mpd 14 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mt4i  131  fin1a2s  8056  gchinf  8295  pwfseqlem4  8300  isprm2lem  12781  pcfac  12963  prmreclem3  12981  sylow1lem1  14925  irredrmul  15505  ioorcl2  18943  itg2gt0  19131  mdegmullem  19480  atom1d  22949  notnot2ALT  28591
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator