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

Theorem mt2d 117
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 115 . 2  |-  ( ph  ->  ( ch  ->  -.  ps ) )
41, 3mpd 15 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  mt2i  118  nsyl3  119  tz7.44-3  6992  sdomdomtr  7569  domsdomtr  7571  infdif  8502  ackbij1b  8532  isf32lem5  8650  alephreg  8870  cfpwsdom  8872  inar1  9064  tskcard  9070  npomex  9285  recnz  10855  rpnnen1lem5  11131  fznuz  11682  uznfz  11683  seqcoll2  12417  ramub1lem1  14546  pgpfac1lem1  17238  lsppratlem6  17911  nconsubb  20009  iunconlem  20013  clscon  20016  xkohaus  20239  reconnlem1  21416  ivthlem2  21949  perfectlem1  23621  lgseisenlem1  23741  ex-natded5.8-2  25256  oddpwdc  28476  erdszelem9  28832  heiborlem8  30480  lcvntr  35164  ncvr1  35410  llnneat  35651  2atnelpln  35681  lplnneat  35682  lplnnelln  35683  3atnelvolN  35723  lvolneatN  35725  lvolnelln  35726  lvolnelpln  35727  lplncvrlvol  35753  4atexlemntlpq  36205  cdleme0nex  36428
  Copyright terms: Public domain W3C validator