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

Theorem mt2d 117
Description: Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)
Hypotheses
Ref Expression
mt2d.1  |-  ( ph  ->  ch )
mt2d.2  |-  ( ph  ->  ( ps  ->  -.  ch ) )
Assertion
Ref Expression
mt2d  |-  ( ph  ->  -.  ps )

Proof of Theorem mt2d
StepHypRef Expression
1 mt2d.1 . 2  |-  ( ph  ->  ch )
2 mt2d.2 . . 3  |-  ( ph  ->  ( ps  ->  -.  ch ) )
32con2d 115 . 2  |-  ( ph  ->  ( ch  ->  -.  ps ) )
41, 3mpd 15 1  |-  ( ph  ->  -.  ps )
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:  mt2i  118  nsyl3  119  tz7.44-3  7076  sdomdomtr  7652  domsdomtr  7654  infdif  8592  ackbij1b  8622  isf32lem5  8740  alephreg  8960  cfpwsdom  8962  inar1  9156  tskcard  9162  npomex  9377  recnz  10945  rpnnen1lem5  11223  fznuz  11771  uznfz  11772  seqcoll2  12495  ramub1lem1  14526  pgpfac1lem1  17104  lsppratlem6  17777  nconsubb  19902  iunconlem  19906  clscon  19909  xkohaus  20132  reconnlem1  21309  ivthlem2  21842  perfectlem1  23482  lgseisenlem1  23602  ex-natded5.8-2  25113  oddpwdc  28271  erdszelem9  28621  heiborlem8  30290  lcvntr  34626  ncvr1  34872  llnneat  35113  2atnelpln  35143  lplnneat  35144  lplnnelln  35145  3atnelvolN  35185  lvolneatN  35187  lvolnelln  35188  lvolnelpln  35189  lplncvrlvol  35215  4atexlemntlpq  35667  cdleme0nex  35890
  Copyright terms: Public domain W3C validator