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  6850  sdomdomtr  7432  domsdomtr  7434  infdif  8366  ackbij1b  8396  isf32lem5  8514  alephreg  8734  cfpwsdom  8736  inar1  8929  tskcard  8935  npomex  9152  recnz  10704  rpnnen1lem5  10970  fznuz  11525  uznfz  11526  seqcoll2  12200  ramub1lem1  14069  pgpfac1lem1  16548  lsppratlem6  17154  nconsubb  18868  iunconlem  18872  clscon  18875  xkohaus  19067  reconnlem1  20244  ivthlem2  20777  perfectlem1  22452  lgseisenlem1  22572  ex-natded5.8-2  23443  oddpwdc  26584  erdszelem9  26934  heiborlem8  28558  lcvntr  32241  ncvr1  32487  llnneat  32728  2atnelpln  32758  lplnneat  32759  lplnnelln  32760  3atnelvolN  32800  lvolneatN  32802  lvolnelln  32803  lvolnelpln  32804  lplncvrlvol  32830  4atexlemntlpq  33282  cdleme0nex  33504
  Copyright terms: Public domain W3C validator