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 15 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mt4i  133  fin1a2s  8250  gchinf  8488  pwfseqlem4  8493  isprm2lem  13041  pcfac  13223  prmreclem3  13241  sylow1lem1  15187  irredrmul  15767  ioorcl2  19417  itg2gt0  19605  mdegmullem  19954  atom1d  23809  notnot2ALT  28324
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator