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  7066  sdomdomtr  7642  domsdomtr  7644  infdif  8580  ackbij1b  8610  isf32lem5  8728  alephreg  8948  cfpwsdom  8950  inar1  9144  tskcard  9150  npomex  9365  recnz  10927  rpnnen1lem5  11203  fznuz  11751  uznfz  11752  seqcoll2  12468  ramub1lem1  14394  pgpfac1lem1  16910  lsppratlem6  17576  nconsubb  19685  iunconlem  19689  clscon  19692  xkohaus  19884  reconnlem1  21061  ivthlem2  21594  perfectlem1  23227  lgseisenlem1  23347  ex-natded5.8-2  24800  oddpwdc  27921  erdszelem9  28271  heiborlem8  29906  lcvntr  33700  ncvr1  33946  llnneat  34187  2atnelpln  34217  lplnneat  34218  lplnnelln  34219  3atnelvolN  34259  lvolneatN  34261  lvolnelln  34262  lvolnelpln  34263  lplncvrlvol  34289  4atexlemntlpq  34741  cdleme0nex  34963
  Copyright terms: Public domain W3C validator