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 16 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  mt2i  112  nsyl3  113  tz7.44-3  6375  sdomdomtr  6948  domsdomtr  6950  infdif  7789  ackbij1b  7819  isf32lem5  7937  alephreg  8158  cfpwsdom  8160  inar1  8351  tskcard  8357  npomex  8574  recnz  10040  rpnnen1lem5  10299  fznuz  10816  uznfz  10817  seqcoll2  11353  ramub1lem1  13021  pgpfac1lem1  15257  lsppratlem6  15853  nconsubb  17097  iunconlem  17101  clscon  17104  xkohaus  17295  reconnlem1  18279  ivthlem2  18760  perfectlem1  20416  lgseisenlem1  20536  ex-natded5.8-2  20775  erdszelem9  23088  heiborlem8  25895  lcvntr  28367  ncvr1  28613  llnneat  28854  2atnelpln  28884  lplnneat  28885  lplnnelln  28886  3atnelvolN  28926  lvolneatN  28928  lvolnelln  28929  lvolnelpln  28930  lplncvrlvol  28956  4atexlemntlpq  29408  cdleme0nex  29630
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator