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

Theorem mt2d 111
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 109 . 2  |-  ( ph  ->  ( ch  ->  -.  ps ) )
41, 3mpd 15 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mt2i  112  nsyl3  113  tz7.44-3  6603  sdomdomtr  7177  domsdomtr  7179  infdif  8023  ackbij1b  8053  isf32lem5  8171  alephreg  8391  cfpwsdom  8393  inar1  8584  tskcard  8590  npomex  8807  recnz  10278  rpnnen1lem5  10537  fznuz  11060  uznfz  11061  seqcoll2  11641  ramub1lem1  13322  pgpfac1lem1  15560  lsppratlem6  16152  nconsubb  17408  iunconlem  17412  clscon  17415  xkohaus  17607  reconnlem1  18729  ivthlem2  19217  perfectlem1  20881  lgseisenlem1  21001  erdszelem9  24665  heiborlem8  26219  lcvntr  29142  ncvr1  29388  llnneat  29629  2atnelpln  29659  lplnneat  29660  lplnnelln  29661  3atnelvolN  29701  lvolneatN  29703  lvolnelln  29704  lvolnelpln  29705  lplncvrlvol  29731  4atexlemntlpq  30183  cdleme0nex  30405
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator