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

Theorem mt4d 132
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 99 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mpd 16 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  mt4i  133  fin1a2s  7994  gchinf  8233  pwfseqlem4  8238  isprm2lem  12713  pcfac  12895  prmreclem3  12913  sylow1lem1  14857  irredrmul  15437  ioorcl2  18875  itg2gt0  19063  mdegmullem  19412  atom1d  22879  notnot2ALT  27329
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator