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

Theorem mt4d 138
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 105 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mpd 15 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  mt4i  139  fin1a2s  8687  gchinf  8928  pwfseqlem4  8933  isprm2lem  13881  pcfac  14072  prmreclem3  14090  sylow1lem1  16210  irredrmul  16914  mdetunilem9  18551  ioorcl2  21178  itg2gt0  21364  mdegmullem  21675  atom1d  25902  notnot2ALT  31537
  Copyright terms: Public domain W3C validator