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  6354  sdomdomtr  6927  domsdomtr  6929  infdif  7768  ackbij1b  7798  isf32lem5  7916  alephreg  8137  cfpwsdom  8139  inar1  8330  tskcard  8336  npomex  8553  recnz  10019  rpnnen1lem5  10278  fznuz  10795  uznfz  10796  seqcoll2  11332  ramub1lem1  13000  pgpfac1lem1  15236  lsppratlem6  15832  nconsubb  17076  iunconlem  17080  clscon  17083  xkohaus  17274  reconnlem1  18258  ivthlem2  18739  perfectlem1  20395  lgseisenlem1  20515  ex-natded5.8-2  20754  erdszelem9  23067  heiborlem8  25874  lcvntr  28346  ncvr1  28592  llnneat  28833  2atnelpln  28863  lplnneat  28864  lplnnelln  28865  3atnelvolN  28905  lvolneatN  28907  lvolnelln  28908  lvolnelpln  28909  lplncvrlvol  28935  4atexlemntlpq  29387  cdleme0nex  29609
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator