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

Theorem mt4d 143
Description: Modus tollens deduction. Deduction form of mt4 142. (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 108 . 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  144  fin1a2s  8844  gchinf  9082  pwfseqlem4  9087  isprm2lem  14616  pcfac  14829  prmreclem3  14847  sylow1lem1  17235  irredrmul  17920  mdetunilem9  19629  ioorcl2  22508  itg2gt0  22702  mdegmullem  23011  atom1d  27989  notnot2ALT  36741  fourierdlem79  37866
  Copyright terms: Public domain W3C validator