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

Theorem mt2d 109
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 107 . 2  |-  ( ph  ->  ( ch  ->  -.  ps ) )
41, 3mpd 14 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  mt2i  110  nsyl3  111  tz7.44-3  6437  sdomdomtr  7010  domsdomtr  7012  infdif  7851  ackbij1b  7881  isf32lem5  7999  alephreg  8220  cfpwsdom  8222  inar1  8413  tskcard  8419  npomex  8636  recnz  10103  rpnnen1lem5  10362  fznuz  10880  uznfz  10881  seqcoll2  11418  ramub1lem1  13089  pgpfac1lem1  15325  lsppratlem6  15921  nconsubb  17165  iunconlem  17169  clscon  17172  xkohaus  17363  reconnlem1  18347  ivthlem2  18828  perfectlem1  20484  lgseisenlem1  20604  ex-natded5.8-2  20817  erdszelem9  23745  heiborlem8  26645  lcvntr  29838  ncvr1  30084  llnneat  30325  2atnelpln  30355  lplnneat  30356  lplnnelln  30357  3atnelvolN  30397  lvolneatN  30399  lvolnelln  30400  lvolnelpln  30401  lplncvrlvol  30427  4atexlemntlpq  30879  cdleme0nex  31101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator