MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mt2d Structured version   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  6658  sdomdomtr  7232  domsdomtr  7234  infdif  8079  ackbij1b  8109  isf32lem5  8227  alephreg  8447  cfpwsdom  8449  inar1  8640  tskcard  8646  npomex  8863  recnz  10335  rpnnen1lem5  10594  fznuz  11119  uznfz  11120  seqcoll2  11703  ramub1lem1  13384  pgpfac1lem1  15622  lsppratlem6  16214  nconsubb  17476  iunconlem  17480  clscon  17483  xkohaus  17675  reconnlem1  18847  ivthlem2  19339  perfectlem1  21003  lgseisenlem1  21123  erdszelem9  24875  heiborlem8  26481  lcvntr  29725  ncvr1  29971  llnneat  30212  2atnelpln  30242  lplnneat  30243  lplnnelln  30244  3atnelvolN  30284  lvolneatN  30286  lvolnelln  30287  lvolnelpln  30288  lplncvrlvol  30314  4atexlemntlpq  30766  cdleme0nex  30988
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator