MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mt4d Structured version   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 15 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mt4i  133  fin1a2s  8286  gchinf  8524  pwfseqlem4  8529  isprm2lem  13078  pcfac  13260  prmreclem3  13278  sylow1lem1  15224  irredrmul  15804  ioorcl2  19456  itg2gt0  19644  mdegmullem  19993  atom1d  23848  notnot2ALT  28550
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator