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  6307  sdomdomtr  6879  domsdomtr  6881  infdif  7719  ackbij1b  7749  isf32lem5  7867  alephreg  8084  cfpwsdom  8086  inar1  8277  tskcard  8283  npomex  8500  recnz  9966  rpnnen1lem5  10225  fznuz  10742  uznfz  10743  seqcoll2  11279  ramub1lem1  12947  pgpfac1lem1  15144  lsppratlem6  15739  nconsubb  16981  iunconlem  16985  clscon  16988  xkohaus  17179  reconnlem1  18163  ivthlem2  18644  perfectlem1  20300  lgseisenlem1  20420  ex-natded5.8-2  20659  erdszelem9  22901  heiborlem8  25708  lcvntr  28017  ncvr1  28263  llnneat  28504  2atnelpln  28534  lplnneat  28535  lplnnelln  28536  3atnelvolN  28576  lvolneatN  28578  lvolnelln  28579  lvolnelpln  28580  lplncvrlvol  28606  4atexlemntlpq  29058  cdleme0nex  29280
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator